proposition: Theorem canonical_reduce : forall (Q : list (poly A0 eqA ltM)) (p q : list (Term A n)), reduce Q p q -> canonical A0 eqA ltM p -> canonical A0 eqA ltM q.
proof: Proof. Proof using plusA os cs. intros Q p q H'; elim H'; auto. intros a b nZb p0 q0 r H'0 H'1 H'2 H'3. apply eqp_imp_canonical with (1 := cs) (p := spminusf A A0 A1 eqA invA minusA multA divA eqA_dec n ltM ltM_dec a b nZb p0 q0); auto. apply canonical_spminusf with (1 := cs); auto. apply canonical_imp_canonical with (a := a); auto. apply canonical_imp_canonical with (a := b); auto. apply inPolySet_imp_canonical with (L := Q); auto. intros a b p0 q0 H'0 H'1 H'2 H'3. apply eqp_imp_canonical with (1 := cs) (p := pX a q0); auto. cut (canonical A0 eqA ltM p0); [ intros C1 | apply canonical_imp_canonical with (a := a) ]; auto. apply ltP_pX_canonical; auto. apply canonical_nzeroP with (ltM := ltM) (p := p0); auto. apply ltP_trans with (y := p0); auto. apply ltP_reduce with (Q := Q); auto. apply (canonical_pX_ltP A A0 eqA); auto. Qed.