proposition: Lemma l8_21 : forall A B C, A <> B -> exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P.
proof: Proof. intros. induction(col_dec A B C). assert (exists C', ~ Col A B C'). eapply not_col_exists. assumption. ex_elim H1 C'. assert ( exists P : Tpoint, (exists T : Tpoint, Perp A B P A /\ Col A B T /\ Bet C' T P)). eapply l8_21_aux. assumption. ex_elim H1 P. ex_and H3 T. exists P. exists C. repeat split. assumption. assumption. apply between_trivial2. eapply l8_21_aux. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR