proposition: Lemma or_lta2_conga : forall A B C D E F, A <> B -> C <> B -> D <> E -> F <> E -> LtA A B C D E F \/ LtA D E F A B C \/ CongA A B C D E F.
proof: Proof. intros. assert(HH:=lea_total A B C D E F). induction HH; auto. induction(conga_dec A B C D E F). right; right. assumption. left. split; assumption. induction(conga_dec A B C D E F). right; right. assumption. right; left. split. assumption. intro. apply H4. apply conga_sym. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2