proposition: Lemma gimel_prop1 x: regular_cardinal x -> gimel_fct x = \2c ^c x.
proof: Proof. by move=> /regular_cardinalP[ic xc]; rewrite /gimel_fct xc infinite_power1_b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)