proposition: Lemma sum_cong2 : forall A B C, Sum O E E' A B C -> (A <> O \/ B <> O) -> (Cong O A B C /\ Cong O B A C).
proof: Proof. intros. apply sum_cong in H. unfold Parallelogram_flat in *. spliter;split;Cong. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg