proposition: Theorem Cantor_normal_form : forall o, zero < o -> nf o -> {a:T1 & {n: nat &{b : T1 | o = omega ^ a * (F (S n)) + b /\ nf (cons a n b) /\ (forall a' n' b', nf (cons a' n' b') -> o = omega ^ a' * (F (S n')) + b' -> a = a' /\ n=n' /\ b = b' )}}}.
proof: Proof. intro ; case o. intro i; case (lt_irr i). intros a n b H H0. exists a;exists n;exists b; split. apply cons_ambiguity;auto. split;[auto|intros a' n' b' H' e']. apply cons_unicity;auto. rewrite <- e'. symmetry;apply cons_ambiguity;auto. Defined.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List