proposition: Lemma even_compare n p: natp p -> evenp n -> n <=c (\2c *c p) +c \1c -> n <=c (\2c *c p).
proof: Proof. move => pa pb; rewrite (half_even pb); set m := (n %/c \2c). move: pb => [pc pd]; move: (NS_quo \2c pc) => mB. case: (cleT_el (CS_nat mB) (CS_nat pa)) => le1 le2. exact (cprod_Mlele (cleR CS2) le1). move /(cleSltP pa): le1 => le3. have aux: natp (\2c *c p +c \1c) by fprops. move: (cprod_Mlele (cleR CS2) le3); rewrite (Nsucc_rw pa). rewrite cprodDr - (csum_nn \1c) csumA - (Nsucc_rw aux). by move /(cleSltP aux) => /(cleNgt le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)