proposition: Lemma cancelNat : forall a b c: nat, true -> a + b = a + c -> b = c.
proof: Proof. move=> a b c; elim: a=>// n /(_ is_true_true) Hn _ H. by apply: Hn; rewrite !addSn in H; move/eq_add_S: H. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun)