proposition: Lemma rem_two_prop1 m i: natp m -> natp i -> (cdouble m) %%c \2c ^c (csucc i) = cdouble (m %%c \2c ^c i).
proof: Proof. move =>mN iN. have p1nz: \2c ^c i <> \0c by apply:cpow_nz; apply: card2_nz. move: (NS_pow NS2 iN) (NS_pow NS2 (NS_succ iN)) => p1N p2N. move:(cdivision mN p1N p1nz). set q := (m %/c \2c ^c i); set r := (m %%c \2c ^c i). move => [qN rN [pa pb]]. have ha:cdivision_prop (cdouble m) (\2c ^c csucc i) q (cdouble r). rewrite - (cdouble_pow2 iN). split; first by rewrite pa - double_sum {1}/cdouble cprodA. by apply /(double_monotone2 rN p1N). by move: (proj2(cquorem_pr (NS_double mN) p2N qN (NS_double rN) ha)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)