proposition: Theorem order_plusP : forall l1 l2 l3 a, plusP 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 os. intros l1 l2 l3 a H'; generalize a; elim H'; auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 a0 H'3 H'4 H'5. apply canonical_cons; auto. apply (canonical_pX_order _ A0 eqA) with (l := l4); auto. apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := pX a1 l4); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 a0 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 a0 H'4 H'5 H'6. apply canonical_cons; auto. apply ltT_eqTr with (a := a1); auto. apply (eqT_sym A n (plusTerm (A:=A) plusA (n:=n) a1 a2)). apply plusTerm_eqT1; auto. apply (canonical_pX_order _ A0 eqA) with (l := l4); auto. apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := pX a1 l4); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 a0 H'3 H'4 H'5. apply canonical_cons; auto. apply (canonical_pX_order _ A0 eqA) with (l := l5); auto. apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := pX a1 l4); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)