proposition: Lemma l4_17 : forall A B C P Q, A<>B -> Col A B C -> Cong A P A Q -> Cong B P B Q -> Cong C P C Q.
proof: Proof. intros. assert (FSC A B C P A B C Q) by (unfold FSC; unfold Cong_3;repeat split; Cong). eapply l4_16; eauto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_cong_bet