proposition: Lemma signEq_refl : forall O E A, O <> E -> Col O E A -> A = O \/ SignEq O E A A.
proof: Proof. intros. assert(HH:= sign_dec O E A H0 H). unfold SignEq. induction HH. { left; auto. } { induction H1. { right; left; auto. } { right; right; auto. } } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order