n m k : nat_gcd (n + k * m) m = nat_gcd n m. Proof. rapply nat_gcd_unique. intros q H1 H2. rapply nat_divides_r_gcd. rapply (nat_divides_add_l _ _ (k * m)). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes