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