proposition: Theorem canonical_minuspf : forall l1 l2 : list (Term A n), canonical A0 eqA ltM l1 -> canonical A0 eqA ltM l2 -> canonical A0 eqA ltM (minuspf l1 l2).
proof: Proof. Proof using plusA os divA cs. intros l1 l2 H' H'0; generalize (minuspf_is_minusP l1 l2); intros u1. apply canonical_minusP with (l1 := l1) (l2 := l2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)