proposition: Lemma cong_cong_half_2 : forall A M B A' M' B', Midpoint M A B -> Midpoint M' A' B' -> Cong A B A' B' -> Cong B M B' M'.
proof: Proof. intros. apply cong_cong_half_1 with A A'. Midpoint. Midpoint. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Tactics.ColR