proposition: Lemma L13 : P beta.
proof: Proof. destruct (cases_for_mult Halpha). - apply L1;auto. - destruct (cases_for_mult Hbeta). + apply L2; auto. + destruct H as [[n Hn] | ]. destruct H0 as [[p Hp] | ]. eapply L3; eauto. destruct H as [[a [p [H1 H2]]] | ]. apply L8 with n a p; auto. destruct H as [a [p [b [H1 [H2 H3]]]]]. apply L11 with n a p b; auto. destruct H. destruct H as [a [n [H1 H2]]]. destruct H0. destruct H. apply L4 with a n zero x; auto. destruct H. destruct H as [b [p [H3 H4]]]. apply L12 with a n zero b p zero; auto. destruct H as [b [p [c [H3 [H4 H5]]]]]. apply L12 with a n zero b p c;auto. destruct H as [a [n [b [H1 [H2 H3]]]]]. destruct H0. destruct H. apply L4 with a n b x; auto. destruct H. destruct H as [c [p [H4 H5]]]. apply L12 with a n b c p zero; auto. destruct H as [c [p [d [H4 [H5 H6]]]]]. apply L12 with a n b c p d;auto. 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)