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