proposition: Theorem unique_decomposition : forall a n b a' n' b', nf (cons a n b) -> nf (cons a' n' b') -> T1omega ^ a * FS n + b = T1omega ^ a' * FS n' + b' -> a = a' /\ n = n' /\ b = b'.
proof: Proof. intros a n b a' n' b' N N'; rewrite <- (cons_def N); rewrite <- (cons_def N'); now injection 1. Qed.
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)