Library ProjectiveGeometry.Plane.P10_complete_quadrilateral_2
Require Export hexamys.
Lemma complete_quadrilateral_2 : hexamy ->
forall A B C A' B' C' II J P Q,
dist6 B C B' C' II J ->
dist6 A B C A' B' C' ->
line A' B' <> line B C ->
is_transverse A' B' C' A B C ->
Col II C C' ->
Col J B B' ->
is_on_inter P B' II C' J ->
is_on_inter Q B II C J ->
Col A P Q.
Proof.
intros.
unfold is_transverse, is_on_inter, dist6 in *.
geo_norm.
remove_line_occ.
create_inter B J C' II X.
collapse.
not_eq l l0.
not_eq x x0.
not_eq x1 x2.
not_eq x4 x5.
hexamy_proof C B J B' C' II B C' J C B' II.
Qed.
Lemma complete_quadrilateral_2 : hexamy ->
forall A B C A' B' C' II J P Q,
dist6 B C B' C' II J ->
dist6 A B C A' B' C' ->
line A' B' <> line B C ->
is_transverse A' B' C' A B C ->
Col II C C' ->
Col J B B' ->
is_on_inter P B' II C' J ->
is_on_inter Q B II C J ->
Col A P Q.
Proof.
intros.
unfold is_transverse, is_on_inter, dist6 in *.
geo_norm.
remove_line_occ.
create_inter B J C' II X.
collapse.
not_eq l l0.
not_eq x x0.
not_eq x1 x2.
not_eq x4 x5.
hexamy_proof C B J B' C' II B C' J C B' II.
Qed.