proposition: Lemma ltR1exp2S s : 1 < exp2R s.+1.
proof: Proof. by apply/(@intR_ltP R 1); rewrite lez_nat (leq_exp2l 1). 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)