proposition: Lemma gimel_prop3 x: infinite_c x -> [/\ (regular_cardinal x -> \2c ^c x = gimel_fct x), (singular_cardinal x -> cpow_less_ecb x -> \2c ^c x = \2c ^<c x) & (singular_cardinal x -> not (cpow_less_ecb x) -> \2c ^c x = gimel_fct (\2c ^<c x))].
proof: Proof. move => icx. move: (ord_index_pr1 icx); set n := (ord_index x); move => [pa pb]. have qa: singular_cardinal x -> limit_ordinal n. by rewrite - pb; apply: singular_limit. move: (gimel_prop pa) => [pc pd pe pf]. rewrite pb in pe pf. split; first by symmetry;apply: gimel_prop1. by move => qb qc; rewrite cpow_less_pr10. by move => qb qc; exact (pf (qa qb) qc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)