proposition: Lemma fromNat_succn n : forall b c, @fromNat n b = fromNat c -> @fromNat n (b.+1) = fromNat(c.+1).
proof: Proof. induction n => //. move => b c EQ. rewrite /fromNat-/fromNat. rewrite /fromNat-/fromNat in EQ. elim: (splitTuple EQ) => [EQ1 EQ2]. simpl in EQ1. simpl in EQ2. specialize (IHn _ _ EQ2). rewrite/= !uphalf_half /=EQ1. case ODD: (odd c). + by rewrite !add1n IHn. + by rewrite !add0n EQ2. 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