proposition: Lemma orthonormal_family_aux : orthonormal_family_axiom <-> (forall A B X P Q, ~ Col P Q X -> Per A X P -> Per A X Q -> Per B X P -> Per B X Q -> Col A B X).
proof: Proof. split. - intros up A B X P Q HNCol HAXP HAXQ HBXP HBXQ. destruct (col_dec A B X) as [|HNCol1]; [assumption|]. exfalso. destruct (segment_construction P X P X) as [P' []]. assert_diffs. destruct (ex_per_cong P X X Q P' X) as [Q']; Col; spliter. assert (HAXQ' : Per Q' X A) by (apply (l11_60 P Q X); Perp; Cop). assert (HBXQ' : Per Q' X B) by (apply (l11_60 P Q X); Perp; Cop). assert (HNCol' : ~ Col P X Q') by (apply one_side_not_col123 with Q; assumption). clear dependent Q. rename Q' into Q. destruct (segment_construction A X P' X) as [A' []]. assert (HAXP' : Per P X A') by (assert_diffs; apply per_col with A; Perp; Col). assert (HAXQ : Per Q X A') by (assert_diffs; apply per_col with A; Perp; Col). assert (HNCol : ~ Col A' B X) by (intro; apply HNCol1; ColR). clear dependent A. rename A' into A. destruct (ex_per_cong A X X B P' X) as [B']; Col; [assert_diffs; auto|]. spliter. assert (HBXP' : Per B' X P) by (apply (l11_60 A B X); Perp; Cop). assert (HBXQ : Per B' X Q) by (apply (l11_60 A B X); Perp; Cop). clear dependent B. rename B' into B. assert (HCong : Cong Q P Q P') by (apply per_double_cong with X; [|split]; Cong). apply (up X P' P Q A B); repeat split; [Cong..| | | | |]; (apply cong_transitivity with P Q; [|Cong]); apply l10_12 with X X; Perp; apply cong_transitivity with P' X; Cong. - intros p4col S U1' U1 U2 U3 U4 H; spliter. assert (HMid : Midpoint S U1 U1') by (split; Cong). assert (HPer21 : Per U2 S U1) by (exists U1'; split; Cong). assert_diffs. absurd (Col U2 U1 S). apply not_col_permutation_5, per_not_col; auto. apply p4col with U3 U4; [apply not_col_permutation_2, per_not_col; auto|..]; apply (l8_10 U2 S U1); trivial; repeat split; CongR. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv