proposition: Lemma cong_cong_half_1 : forall A M B A' M' B', Midpoint M A B -> Midpoint M' A' B' -> Cong A B A' B' -> Cong A M A' M'.
proof: Proof. intros. unfold Midpoint in *. spliter. assert(exists M'', Bet A' M'' B' /\ Cong_3 A M B A' M'' B'). eapply l4_5. assumption. assumption. ex_and H4 M''. assert (Midpoint M'' A' B'). unfold Midpoint. split. assumption. unfold Cong_3 in H5. spliter. eapply cong_transitivity. apply cong_symmetry. apply H5. eapply cong_transitivity. apply H3. assumption. assert(M'=M''). eapply l7_17; unfold Midpoint; split. apply H0. apply H2. apply H4. unfold Midpoint in H6. spliter. assumption. subst M''. unfold Cong_3 in H5. spliter. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR