isinj_nat_add_r@{} k : IsInjective (fun x => nat_add x k). Proof. intros x y H. nrapply (isinj_nat_add_l k). lhs nrapply nat_add_comm. lhs nrapply H. nrapply nat_add_comm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids