n m k : k <= n -> (n + m) - k = (n - k) + m. Proof. intro l. rewrite nat_add_comm. lhs rapply nat_sub_l_add_r. apply nat_add_comm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids