proposition: Lemma L9 : forall n c, nf c -> c <> zero -> FS n * c <> zero.
proof: Proof. intros n c H H0; destruct (cases_for_mult H) as [| H1]. - contradiction. - destruct H1 as [H1 | [ H1 | H1]]. + destruct H1; subst; discriminate. + destruct H1 as [a [p [H2 H3]]]; subst; cbn. destruct a;discriminate. + destruct H1 as [a [p [b [H2 [H3 H4]]]]]; subst; cbn. destruct a; [ now destruct H2| 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)