proposition: Theorem order_minusP : forall (l1 l2 l3 : list (Term A n)) (a : Term A n), minusP l1 l2 l3 -> canonical A0 eqA ltM (pX a l1) -> canonical A0 eqA ltM (pX a l2) -> canonical A0 eqA ltM l3 -> canonical A0 eqA ltM (pX a l3).
proof: Proof. Proof using plusA os eqA_dec divA cs. intros l1 l2 l3 a H'; elim H'; auto. intros l4 H'0 H'1 H'2. cut (canonical A0 eqA ltM l4); try apply canonical_imp_canonical with (a := a); auto; intros C0. apply canonical_pX_eqT with (a := multTerm (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) a); auto. change (canonical A0 eqA ltM (mults (A:=A) multA (n:=n) (invTerm (A:=A) invA (n:=n) (T1 A1 n)) (pX a l4))) in |- *; auto. apply (eqT_sym A n); apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) a); auto. apply (T1_eqT A A1 eqA); auto. apply canonical_nzeroP with (ltM := ltM) (p := l4); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5. apply canonical_cons; auto. apply (canonical_pX_order A A0 eqA) with (ltM := ltM) (l := l4); auto. apply canonical_nzeroP with (ltM := ltM) (p := pX a1 l4); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5 H'6. apply H'1; auto. apply canonical_skip_fst with (b := a1); auto. apply canonical_skip_fst with (b := a2); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5 H'6. apply canonical_cons; auto. apply minusTerm_ltT_l; auto. apply (canonical_pX_order A A0 eqA) with (l := l4); auto. apply canonical_nzeroP with (ltM := ltM) (p := pX a1 l4); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5. apply canonical_cons; auto. apply invTerm_ltT_l; auto. apply (canonical_pX_order A A0 eqA) with (l := l5); auto. apply canonical_nzeroP with (ltM := ltM) (p := pX a1 l4); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)