proposition: Lemma length_eq_cong_1 : forall O E E' A B C D AB, Length O E E' A B AB -> Length O E E' C D AB -> Cong A B C D.
proof: Proof. intros. unfold Length in *. spliter. apply cong_transitivity with O AB;Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order