proposition: Lemma upper_dim_stab : ~ ~ upper_dim_axiom -> upper_dim_axiom.
proof: Proof. intros nnupper A B C P Q HPQ H1 H2 H3. destruct (col_dec A B C) as [|HNCol]; auto. exfalso. apply nnupper. intro upper. apply HNCol. apply upper with P Q; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane