proposition: Lemma leRexp2 s1 s2 : (s1 <= s2)%N -> exp2R s1 <= exp2R s2.
proof: Proof. by move=> le_s12; apply/intR_leP; rewrite lez_nat leq_exp2l. 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)