n m : nat_gcd n (m + n) = nat_gcd n m. Proof. lhs nrapply nat_gcd_comm. rhs nrapply nat_gcd_comm. nrapply nat_gcd_l_add_r. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes