Coq/Rocq: divand

Stream: LFTCM 2024

[Florent Schaffhauser]

I am trying to complete the proof of Lemma divand and here's where I am at:

Lemma divand : forall (m n : nat), 2 %| n /\ 3 %| m -> 6 %| n * m .
Proof.
move=> m n. move=> H.
move: H. move=> [/dvdnP [x A] /dvdnP [y B]].
rewrite A B.
apply /dvdnP.
Admitted.

In Lean, I would carry on by writing use (x * y) and conclude by a computation.

Is there something similar to the use tactic here? Also, what would be a more idiomatic way of writing the proof?

[Florent Schaffhauser]

Cyril told me during the break: the Coq equivalent of use (x * y) is exists (x * y).

Comes with no guarantees, apologies if I misunderstood! :pray:

[Notification Bot]

2 messages were moved here from #LFTCM 2024 > Coq/Rocq tutorial and practice by Cyril Cohen.

[Cyril Cohen]

Flo (Florent Schaffhauser) said:

Cyril told me during the break: the Coq equivalent of use (x * y) is exists (x * y).

Comes with no guarantees, apologies if I misunderstood! :pray:

It's not strictly equivalent, use does strictly more, but that's a first good approximation.