proposition: Lemma or_lt_cong_gt : forall A B C D, Lt A B C D \/ Gt A B C D \/ Cong A B C D.
proof: Proof. intros. assert(HH:= le_cases A B C D). induction HH. induction(cong_dec A B C D). right; right. assumption. left. unfold Lt. split; assumption. induction(cong_dec A B C D). right; right. assumption. right; left. unfold Gt. unfold Lt. split. assumption. intro. apply H0. apply cong_symmetry. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col