proposition: Theorem ltP_divP_pX : forall (a b : Term A n) (p q : list (Term A n)), canonical A0 eqA ltM (pX a p) -> canonical A0 eqA ltM (pX b q) -> divP A A0 eqA multA divA n a b -> ltP (A:=A) (n:=n) ltM q (pX a p).
proof: Proof. Proof using plusA os minusA ltM_dec invA cs A1. intros a b p; case p; auto. intros q H' H'0 H'1; try assumption. change (ltP (A:=A) (n:=n) ltM q (pX a (pO A n))) in |- *; auto. apply (canonical_pX_ltP A A0 eqA); apply divP_ltT_comp with (b := b); auto. intros a0 l q H' H'0 H'1; apply ltP_trans with (y := pX a (pO A n)); auto. apply (canonical_pX_ltP A A0 eqA); apply divP_ltT_comp with (b := b); auto. change (ltP (A:=A) (n:=n) ltM (pX a (pO A n)) (pX a (pX a0 l))) in |- *; auto. Qed.