proposition: Lemma five_segment_with_def : forall A B C D A' B' C' D', OFSC A B C D A' B' C' D' -> A<>B -> Cong C D C' D'.
proof: Proof. unfold OFSC. intros;spliter. apply (five_segment A A' B B'); assumption. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish