proposition: Lemma gimel_prop2 x: infinite_c x -> gimel_fct x <=c \2c ^c x.
proof: Proof. move=> ic; rewrite /gimel_fct - (infinite_power1_b ic). move: (cofinality_small ic) => cg. apply: cpow_Mlele => //; [ by apply: infinite_nz | apply: (cleR (proj1 ic))]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)