proposition: Theorem eqp_imp_canonical : forall p q, eqP p q -> canonical A0 eqA ltM p -> canonical A0 eqA ltM q.
proof: Proof. Proof using plusA multA minusA invA eqA_dec divA cs A1. intros p q H'; elim H'; auto. intros ma mb p0 q0 H'0 H'1 H'2 H'3. apply canonical_pX_eqT with (a := ma); auto. apply ltP_pX_canonical; auto. apply H'2. apply canonical_imp_canonical with (a := ma); auto. apply (canonical_nzeroP A A0 eqA n ltM ma p0); auto. apply ltp_eqp_comp with (p := p0) (q := pX ma (pO A n)); auto. apply canonical_pX_ltP with (1 := H'3). apply canonical_imp_canonical with (a := ma); auto. apply canonicalp1; auto. apply (canonical_nzeroP A A0 eqA n ltM ma p0); auto. apply nzeroP_comp_eqTerm with (1 := cs) (a := ma); auto. apply (canonical_nzeroP A A0 eqA n ltM ma p0); auto. Qed.
imports: Coq(Arith Compare_dec)