proposition: Lemma cong_perp_or_mid : forall A B M X, A <> B -> Midpoint M A B -> Cong A X B X -> X = M \/ ~Col A B X /\ Perp_at M X M A B.
proof: Proof. intros. induction(col_dec A B X). left. assert(A = B \/ Midpoint X A B). apply l7_20; Col. Cong. induction H3. contradiction. apply (l7_17 A B); auto. right. split; auto. assert(Col M A B). unfold Midpoint in *. spliter; Col. assert_diffs. assert(Per X M A) by (unfold Per;exists B;split; Cong). apply per_perp_in in H4. apply perp_in_right_comm in H4. apply(perp_in_col_perp_in X M A M B M); Col. intro;treat_equalities. apply H2; Col. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR