nat_sub_comm_r@{} n m k : n - m - k = n - k - m. Proof. lhs_V nrapply nat_sub_r_add. rewrite nat_add_comm. nrapply nat_sub_r_add. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids