n m p (H : forall q, (q | n) -> (q | m) -> (q | p)) : (p | n) -> (p | m) -> nat_gcd n m = p. Proof. intros H1 H2. rapply nat_divides_antisym. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes