proposition: Theorem Cantor_normal_form : forall o, lt zero o -> nf o -> {a:T1 & {n: nat & {b : T1 | o = T1omega ^ a * FS n + b /\ nf (cons a n b) }}}.
proof: Proof. intro ; case o. - intro H. now apply lt_irrefl in H. - intros a n b H H0; exists a;exists n;exists b; split. + now apply cons_def. + assumption. Defined.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)