proposition: Lemma approx_halfz s x m : approx s.+1 x m -> approx s x (m %/ 2)%Z%N.
proof: Proof. rewrite /approx exp2RS -mulRA [m : R]intR_addbit -/intRR modz2. move: {s x}(_ * x) {m}(odd `|m|) (m %/ 2)%Z%N => x b m [Hxm Hmx]. split; rewrite -(leR_pmul2l _ _ ltR02). by apply: leR_trans Hxm; rewrite -subR_ge0 addRK; apply: leR0n. apply: (ltR_le_trans Hmx); rewrite mulRDr mulR1 addRCA -addRA leR_add2r. by apply/(@intR_leP R _ 1); rewrite lez_nat leq_b1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)