proposition: Lemma cong2_lea__le : forall A B C D E F : Tpoint, Cong A B D E -> Cong A C D F -> LeA F D E C A B -> Le E F B C.
proof: Proof. intros. assert(LtA F D E C A B \/ CongA F D E C A B). { unfold LtA. induction (conga_dec F D E C A B). { right; assumption. } { left. split; auto. } } induction H2. { assert(Lt E F B C). { apply(t18_18 A B C D E F);auto. } apply lt__le. assumption. } assert(Cong F E C B /\ (F <> E -> CongA D F E A C B /\ CongA D E F A B C)). apply(l11_49 F D E C A B); Cong. spliter. unfold Le. exists C. split;Cong. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order