proposition: Lemma fact_greater_geom i : i.+1`!%:R >= (3%:Q / 2%:Q) ^+ i.
proof: Proof. elim: i => // i IHi; rewrite exprS factS natrM; apply: ler_pM IHi => //. by rewrite ler_pdivrMr ?ltr0n // mulr_natr -mulrnA ler_nat. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith