proposition: Theorem canonical_minusP : forall l1 l2 l3 : list (Term A n), minusP l1 l2 l3 -> canonical A0 eqA ltM l1 -> canonical A0 eqA ltM l2 -> canonical A0 eqA ltM l3.
proof: Proof. Proof using plusA os eqA_dec divA cs. intros l1 l2 l3 H'; elim H'; auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4. apply order_minusP with (l1 := l4) (l2 := pX a2 l5); auto. apply canonical_cons; auto. apply canonical_nzeroP with (ltM := ltM) (p := l4); auto. apply H'2; auto. apply canonical_imp_canonical with (a := a1); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5. apply H'1; auto. apply canonical_imp_canonical with (a := a1); auto. apply canonical_imp_canonical with (a := a2); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5. apply order_minusP with (l1 := l4) (l2 := l5); auto. apply canonical_pX_eqT with (a := a1); auto. apply (eqT_sym A n); apply minusTerm_eqT; auto. apply canonical_pX_eqT with (a := a2); auto. apply (eqT_trans A n) with (y := a1); apply (eqT_sym A n); auto. apply minusTerm_eqT; auto. apply H'1. apply canonical_imp_canonical with (a := a1); auto. apply canonical_imp_canonical with (a := a2); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4. apply order_minusP with (l1 := pX a1 l4) (l2 := l5); auto. apply canonical_pX_eqT with (a := a2); auto. apply canonical_cons; auto. apply canonical_nzeroP with (ltM := ltM) (p := l5); auto. apply nZero_invTerm_nZero with (1 := cs); auto. apply canonical_nzeroP with (ltM := ltM) (p := l5); auto. apply canonical_pX_eqT with (a := a2); auto. apply nZero_invTerm_nZero with (1 := cs); auto. apply canonical_nzeroP with (ltM := ltM) (p := l5); auto. apply H'2; auto. apply canonical_imp_canonical with (a := a2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)