proposition: Lemma addnCA: forall m n p, m + (n + p) = n + (m + p).
proof: Proof. move=>m n. elim: m=>[ | m Hm ] p. by rewrite !add0n. by rewrite !addSnnS -addnS. Restart. by move=>m n; elim: m=>[ | m Hm ] p; rewrite ?add0n ?addSnnS -?addnS. Qed.
imports: mathcomp(ssreflect ssrfun eqtype ssrnat ssrbool)