Library ProjectiveGeometry.Plane.P06_angle_line
Require Export hexamys.
Lemma angle_line : hexamy -> forall O S O' A A' R M X Y,
dist6 O S O' A A' R ->
line A R <> line O S ->
Col O O' S ->
Col R A A' ->
Col M O A ->
Col M O' A' ->
Col X S A ->
Col X R O' ->
Col Y S A' ->
Col Y R O ->
Col M X Y.
Proof.
intros.
unfold dist6 in *.
geo_norm.
create_inter A R O' S Z.
collapse.
remove_line_occ.
not_eq x3 x4.
not_eq x x0.
not_eq x1 x2.
hexamy_proof O A R A' O' S O A S A' O' R.
Qed.
Lemma angle_line : hexamy -> forall O S O' A A' R M X Y,
dist6 O S O' A A' R ->
line A R <> line O S ->
Col O O' S ->
Col R A A' ->
Col M O A ->
Col M O' A' ->
Col X S A ->
Col X R O' ->
Col Y S A' ->
Col Y R O ->
Col M X Y.
Proof.
intros.
unfold dist6 in *.
geo_norm.
create_inter A R O' S Z.
collapse.
remove_line_occ.
not_eq x3 x4.
not_eq x x0.
not_eq x1 x2.
hexamy_proof O A R A' O' S O A S A' O' R.
Qed.