proposition: Lemma median_planes_implies_upper_dim : median_planes_axiom -> upper_dim_3_axiom.
proof: Proof. intros mp A B C P Q R HPQ HQR HPR; intros. destruct (col_dec A B C); trivial. exfalso. apply HQR. destruct (midpoint_existence P Q) as [X]. apply symmetric_point_uniqueness with P X; trivial. destruct (midpoint_existence P R) as [Y]. replace X with Y; trivial. apply (l8_7 P); apply l8_2. - apply l11_60 with A B C; [|exists R; split..|]; trivial. apply mp with P Q; Cong. - apply l11_60 with A B C; [|exists Q; split..|]; trivial. apply mp with P R; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Utils.all_equiv