proposition: Lemma per_double_cong : forall A B C C', Per A B C -> Midpoint B C C' -> Cong A C A C'.
proof: Proof. intros. unfold Per in H. ex_and H C''. assert (C' = C''). eapply l7_9. apply l7_2. apply H0. apply l7_2. assumption. subst C''. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR