proposition: Lemma upper_dim_implies_orthonormal_family_axiom : upper_dim_3_axiom -> orthonormal_family_axiom.
proof: Proof. rewrite orthonormal_family_aux. intros up A B X P Q HNCol HAXP HAXQ HBXP HBXQ. destruct (segment_construction Q X X P) as [Q' []]. assert (HNCol' : ~ Col P Q' X) by (intro; apply HNCol; ColR). assert (HAXQ' : Per A X Q') by (assert_diffs; apply per_col with Q; Col). assert (HBXQ' : Per B X Q') by (assert_diffs; apply per_col with Q; Col). clear dependent Q. destruct (symmetric_point_construction P X) as [R]. assert_diffs. apply up with P Q' R. auto. intro; subst; apply HNCol'; Col. auto. apply l10_12 with X X; Cong. apply l10_12 with X X; Cong. Cong. apply per_double_cong with X; assumption. apply per_double_cong with X; assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv