proposition: Lemma L10 : forall a n b c, nf c -> nf (cons a n b) -> a <>zero -> c <> zero -> cons a n b * c <> zero.
proof: Proof. intros a n b c H H0 H1 H2; destruct (cases_for_mult H). - subst; now destruct H2. - destruct H3 as [H3 | [H3 | H3]]. + destruct H3; subst; rewrite L03; auto; discriminate. + destruct H3 as [d [p [H4 H5]]]; subst; rewrite L05; auto; discriminate. + destruct H3 as [d [p [e [H4 [H5 H6]]]]]; subst; rewrite L05; auto; discriminate. 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)