proposition: Lemma PlgExABC2: forall A B C, ~Col A B C -> Cong A B B C -> exists D, Plg A B C D.
proof: Proof. intros A B C HC H. unfold Plg in *. assert(Is_on_perp_bisect B A C). exact H. destruct (midpoint_existence A B) as [X H1]. destruct (l10_2_existence A C B) as [D H3]. unfold Reflect in H3. unfold ReflectL in H3. induction (eq_dec_points A C). case H3. - intros. tauto. - intros. unfold Midpoint in H4. destruct (midpoint_existence A C) as [Y H5]. destruct (symmetric_point_construction B Y) as [E H6]. exists E. assert(B <> E). induction (eq_dec_points B E). subst E. assert(Y = B). apply l7_3. exact H6. subst Y. assert(Col A B C). Col. tauto. tauto. split. tauto. exists Y. tauto. - intros. destruct H3. destruct H3;destruct H4;destruct H4. destruct H4. unfold Midpoint in H4. destruct (midpoint_existence A C) as [Y H7]. destruct (symmetric_point_construction B Y) as [E H8]. exists E. assert(B <> E). induction (eq_dec_points B E). subst E. assert(Y = B). apply l7_3. exact H8. subst Y. assert(Col A B C). Col. tauto. tauto. split. tauto. exists Y. tauto. exists D. split. tauto. exists A. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.perp_bisect