proposition: Theorem ppc_is_ppcm : forall a b : Term A n, ~ zeroP (A:=A) A0 eqA (n:=n) a -> ~ zeroP (A:=A) A0 eqA (n:=n) b -> ppcm a b (ppc a b).
proof: Proof. Proof using plusA minusA invA cs. intros a b nZa nZb; apply ppcm0; auto. intros r H'1 H'2; inversion H'1; inversion H'2. cut (~ zeroP (A:=A) A0 eqA (n:=n) (ppc a b)); [ intros nZppab | auto ]. apply divTerm_def with (nZb := nZppab); auto. apply divTerm_ppc with (nZa := nZa) (nZb := nZb); auto. apply ppc_nZ; auto. apply divTerm_def with (nZb := nZa); auto. apply ppc_nZ; auto. apply divTerm_ppcl; auto. apply divTerm_def with (nZb := nZb); auto. apply ppc_nZ; auto. apply divTerm_ppcr; auto. Qed.
imports: Coq(Relation_Definitions List) Buchberger(CoefStructure moreCoefStructure OrderStructure) Buchberger(Monomials Term)