proposition: Lemma projp_lt : forall P Q A T, Cong P A Q A -> Projp A T P Q -> Lt T A P A.
proof: Proof. intros. unfold Projp in H0. spliter. induction H1. { spliter. induction(eq_dec_points P T). { subst T. assert(Lt Q P Q A /\ Lt A P Q A). { apply(per_lt Q P A). auto. apply perp_distinct in H2. tauto. Perp. } spliter. unfold Lt in H4. spliter. apply False_ind. apply H5. Cong. } { assert(Lt P T P A /\ Lt A T P A). { apply(per_lt P T A); auto. apply perp_distinct in H2. tauto. apply (perp_col _ _ _ _ T) in H2; Perp. } spliter. apply lt_left_comm. auto. } } { spliter. subst T. induction(eq_dec_points P A). subst P. apply cong_symmetry in H. apply cong_identity in H. subst Q. tauto. apply lt1123; auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order