proposition: Theorem divP_is_not_order : forall a b : Term A n, divP A A0 eqA multA divA n a b -> ~ ltT ltM a b.
proof: Proof. Proof using plusA os minusA ltM_dec invA cs A1. intros a b H'; inversion H'. case (ltT_dec A n ltM ltM_dec (T1 A1 n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb)); [ intros tmp; case tmp; clear tmp | idtac ]; intros H'2; auto. apply ltT_not_ltT; auto. apply ltT_eqTl with (a := multTerm (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb) b); auto. apply (eqT_sym A n); apply (eqTerm_imp_eqT A eqA); auto. apply ltT_eqTr with (a := multTerm (A:=A) multA (n:=n) (T1 A1 n) b); auto. apply (eqT_sym A n); apply (eqTerm_imp_eqT A eqA); apply T1_multTerm_l with (1 := cs); auto. apply multTerm_ltT_r with (1 := os); auto. elim (T1_is_min_ltT A A1) with (a := divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb) (1 := os); auto. apply ltT_not_eqT; auto. apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) (divTerm (A:=A) (A0:=A0) (eqA:=eqA) divA (n:=n) a (b:=b) nZb) b); auto. apply (eqTerm_imp_eqT A eqA); auto. apply (eqT_trans A n) with (y := multTerm (A:=A) multA (n:=n) (T1 A1 n) b); auto. apply (eqT_sym A n); auto. apply (eqT_sym A n); apply (eqTerm_imp_eqT A eqA); auto. Qed.