proposition: Lemma length_leP_le_1 : forall O E E' A B C D AB CD, Length O E E' A B AB -> Length O E E' C D CD -> LeP O E E' AB CD -> Le A B C D.
proof: Proof. intros. unfold Length in *. spliter. assert(Bet O AB CD). apply (leP_bet O E E'); assumption. prolong D C M' A B. assert(HH:=symmetric_point_construction M' C). ex_and HH M. unfold Midpoint in H11. spliter. assert(Cong A B C M). apply (cong_transitivity _ _ C M'); Cong. apply(le_transitivity _ _ C M). unfold Le. exists M. split; Between. assert(Le O AB O CD). unfold Le. exists AB. split; Cong. apply(l5_6 O AB O CD C M C D); Cong. apply (cong_transitivity _ _ A B); Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order