proposition: Theorem canonical_plusP : forall l1 l2 l3, plusP l1 l2 l3 -> canonical A0 eqA ltM l1 -> canonical A0 eqA ltM l2 -> canonical A0 eqA ltM l3.
proof: Proof. Proof using os. intros l1 l2 l3 H'; elim H'; auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4; try assumption. apply order_plusP with (l1 := l4) (l2 := pX a2 l5); auto. apply canonical_cons; auto. apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := l4); auto. apply H'2; auto. apply (canonical_imp_canonical _ A0 eqA _ ltM) 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 _ A0 eqA _ ltM) with (a := a1); auto. apply (canonical_imp_canonical _ A0 eqA _ ltM) with (a := a2); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4 H'5. apply order_plusP with (l1 := l4) (l2 := l5); auto. apply canonical_pX_eqT with (a := a1); auto. apply (eqT_sym A n (plusTerm (A:=A) plusA (n:=n) a1 a2)). apply plusTerm_eqT1; auto. apply canonical_pX_eqT with (a := a2); auto; auto. apply (eqT_sym A n (plusTerm (A:=A) plusA (n:=n) a1 a2)). apply plusTerm_eqT2; auto. apply H'1. apply (canonical_imp_canonical _ A0 eqA _ ltM) with (a := a1); auto. apply (canonical_imp_canonical _ A0 eqA _ ltM) with (a := a2); auto. intros a1 a2 l4 l5 l6 H'0 H'1 H'2 H'3 H'4. apply order_plusP with (l1 := pX a1 l4) (l2 := l5); auto. apply canonical_cons; auto. apply (canonical_nzeroP _ A0 eqA _ ltM) with (p := l5); auto. apply H'2; auto. apply canonical_imp_canonical with (a := a2); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)