proposition: Theorem ltp_eqp_comp : forall p q r s, ltP (A:=A) (n:=n) ltM p q -> canonical A0 eqA ltM p -> canonical A0 eqA ltM q -> eqP p r -> eqP q s -> ltP (A:=A) (n:=n) ltM r s.
proof: Proof. intros p q r s H'; generalize r s; elim H'; clear r s H'; auto. intros x p0 r s H H0 H1; inversion H1. intros H4; inversion H4; apply ltPO. intros x y p0 q0 H r s H0 H1 H2 H3; inversion_clear H2; try discriminate; inversion_clear H3; try discriminate; auto. apply ltP_hd. apply ltT_eqTl with (a := y); auto. apply ltT_eqTr with (a := x); auto. intros x y p0 q0 H H0 H1 r s H2 H3 H4 H5; inversion_clear H4; try discriminate; inversion_clear H5; try discriminate. apply ltP_tl; auto. apply (eqT_trans A n) with (y := y); auto. apply (eqT_trans A n) with (y := x); auto. apply (eqT_sym A n); auto. apply H1; auto. apply canonical_imp_canonical with (a := x); auto. apply canonical_imp_canonical with (a := y); auto. Qed.
imports: Coq(Arith Compare_dec)