n m : nat_gcd n m = 0 -> n = 0. Proof. intros H. generalize (nat_divides_l_gcd_l n m). rewrite H. intros [x p]. exact (p^ @ nat_mul_zero_r _). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes