proposition: Lemma fromNat_addn n : forall a b c, @fromNat n b = fromNat c -> @fromNat n (a+b) = fromNat(a+c).
proof: Proof. induction a => //. move => b c EQ. rewrite -addn1 -!addnA !add1n. apply IHa. by apply fromNat_succn. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec