n m : nat_gcd n m = 0 <-> n = 0 /\ m = 0. Proof. split. - split. + by apply (nat_gcd_is_zero_l _ m). + by apply (nat_gcd_is_zero_r n). - intros [-> ->]. reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes