proposition: Lemma expe_fusc n: natp n -> Nbexp n = fusc (csucc n).
proof: Proof. move: n. suff: forall n, natp n -> forall k, k <=c n -> Nbexp k = fusc (csucc k). move => H n nN; apply:(H n nN); fprops. apply: Nat_induction. by move => k /cle0 ->; rewrite succ_zero fusc1 expe_0. move => n nN Hrec k lkn;case: (equal_or_not k (csucc n)) => ekn; last first. by apply: Hrec; apply /(cltSleP nN). move:(NS_half nN) => hn. rewrite ekn; case: (cdouble_halfV nN) => eq1; rewrite eq1. rewrite (expe_odd hn) - (double_succ hn) (fusc_even (NS_succ hn)). by apply: Hrec; apply: cle_halfn_n. rewrite - (double_succ hn) (expe_even hn) (fusc_odd (NS_succ hn)). rewrite csumC (Hrec _ (cle_halfn_n nN)) Hrec //. by rewrite eq1;apply/cleSS; rewrite - eq1; apply: cle_n_doublen. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)