proposition: Theorem eqp_pluspf_com_r : forall p q r, eqP A eqA n p q -> canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> canonical A0 eqA ltM r -> eqP A eqA n (pluspf r p) (pluspf r q).
proof: Proof. Proof using os multA minusA invA divA cs A1. intros p q r H'; generalize r; elim H'; clear r H'. intros r H' H'0 H'1; rewrite <- pO_pluspf_inv2; auto. intros ma mb p0 q0 H' H'0 H'1 r H'2 H'3 H'4. cut (canonical A0 eqA ltM p0); [ intros C0 | apply canonical_imp_canonical with (a := ma) ]; auto. cut (canonical A0 eqA ltM q0); [ intros C1 | apply canonical_imp_canonical with (a := mb) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) ma); [ intros nZ0 | apply (canonical_nzeroP _ A0 eqA n ltM) with (p := p0) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) mb); [ intros nZ1 | apply (canonical_nzeroP _ A0 eqA n ltM) with (p := q0) ]; auto. generalize H'4; elim r; clear H'4 r. intros H'4; rewrite <- pO_pluspf_inv1; rewrite <- pO_pluspf_inv1; auto. intros a l H'4 H'5. cut (canonical A0 eqA ltM l); [ intros C2 | apply canonical_imp_canonical with (a := a) ]; auto. cut (~ zeroP (A:=A) A0 eqA (n:=n) a); [ intros nZ2 | apply (canonical_nzeroP _ A0 eqA n ltM) with (p := l) ]; auto. change (eqP A eqA n (pluspf (pX a l) (pX ma p0)) (pluspf (pX a l) (pX mb q0))) in |- *. case (ltT_dec A n ltM ltM_dec ma a); [ intros H0; case H0; clear H0 | idtac ]; intros H0. cut (ltT ltM mb a); [ intros Or0 | idtac ]. rewrite <- (pluspf_inv1_eq a ma l p0); auto. rewrite <- (pluspf_inv1_eq a mb l q0); auto. apply eqT_compat_ltTl with (b := ma); auto. apply (eqTerm_imp_eqT _ eqA n); auto. cut (ltT ltM a mb); [ intros Or0 | idtac ]; auto. rewrite <- (pluspf_inv2_eq a ma l p0); auto. rewrite <- (pluspf_inv2_eq a mb l q0); auto. apply eqT_compat_ltTr with (b := ma); auto. apply (eqTerm_imp_eqT _ eqA n); auto. cut (eqTerm eqA (plusTerm (A:=A) plusA (n:=n) a ma) (plusTerm (A:=A) plusA (n:=n) a mb)); [ intros eqTerm0 | idtac ]; auto. case (zeroP_dec A A0 eqA eqA_dec n (plusTerm (A:=A) plusA (n:=n) a ma)); intros Z0. rewrite <- (pluspf_inv3a_eq a ma l p0); auto. rewrite <- (pluspf_inv3a_eq a mb l q0); auto. apply (eqT_trans A n) with (y := ma); auto; apply (eqT_sym A n); auto. apply (eqTerm_imp_eqT _ eqA n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a ma); auto. apply (eqT_sym A n); auto. rewrite <- (pluspf_inv3b_eq a ma l p0); auto. rewrite <- (pluspf_inv3b_eq a mb l q0); auto. apply (eqT_trans A n) with (y := ma); auto. apply (eqT_sym A n); auto. apply (eqTerm_imp_eqT _ eqA n); auto. red in |- *; intros H'6; apply Z0. apply zeroP_comp_eqTerm with (1 := cs) (a := plusTerm (A:=A) plusA (n:=n) a mb); auto. apply plusTerm_comp_r with (1 := cs); auto. change (eqT a mb) in |- *. apply (eqT_trans A n) with (y := ma); auto. apply (eqT_sym A n); auto. apply (eqTerm_imp_eqT _ eqA n); auto. apply (eqT_sym A n); auto. apply (eqTerm_sym _ _ _ _ _ _ _ _ _ cs n); auto. apply (eqT_sym A n); auto. apply plusTerm_comp_r with (1 := cs); auto. apply (eqT_sym A n); auto. change (eqT a mb) in |- *. apply (eqT_trans A n) with (y := ma); auto. apply (eqT_sym A n); auto. apply (eqTerm_imp_eqT _ eqA n); auto. Qed.
imports: Coq(Arith) Buchberger(LetP)