proposition: Lemma cases_for_mult (alpha : T1) : nf alpha -> alpha = zero \/ (exists n : nat, alpha = FS n) \/ (exists a n, a <> zero /\ alpha = cons a n zero) \/ (exists a n b, a <> zero /\ b <> zero /\ alpha = cons a n b).
proof: Proof. destruct alpha. - now left. - right. destruct alpha1. left; exists n. apply nf_of_finite in H. now subst. right. destruct alpha2. left . exists (cons alpha1_1 n0 alpha1_2),n. split;[discriminate|trivial]. right ; exists (cons alpha1_1 n0 alpha1_2), n, (cons alpha2_1 n1 alpha2_2). split;[discriminate|trivial]. split;[discriminate|trivial]. 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)