proposition: Lemma natpluslcan (a b c : nat) (is : c + a = c + b) : a = b.
proof: Proof. intros. rewrite (natpluscomm _ _) in is. rewrite (natpluscomm c b) in is. apply (natplusrcan a b c is). Defined.
imports: UniMath.Foundations.Sets