Library ProjectiveGeometry.Plane.P14_pseudo_midpoint
Require Export hexamys.
Lemma pseudo_midpoint : hexamy -> forall II J K A B P Q H M L N O,
dist6 P M L Q N H ->
dist6 A B II J O Q ->
A<>K -> B<>K ->
is_on_inter P II B J A ->
is_on_inter Q II A J B ->
is_on_inter O M N P Q ->
is_on_inter H II B A K ->
is_on_inter M B K J A ->
is_on_inter N A K J B ->
is_on_inter L A II K B ->
Col II J K ->
Col O A B.
Proof.
intro Hhex;intros.
geo_norm.
create_line M L lML.
create_line H N lHN.
create_line L Q lLQ.
create_line H P lHP.
create_line P M lPM.
create_line Q N lQN.
cases_line lML lHN.
solve_col.
not_eq x12 x11.
not_eq x12 x10.
not_eq lLQ x11.
not_eq x3 x11.
not_eq lLQ lHN.
not_eq lPQ lMN.
not_eq x8 x7.
collapse.
hexamy_proof P M L Q N H P Q L M N H.
Qed.
Lemma pseudo_midpoint : hexamy -> forall II J K A B P Q H M L N O,
dist6 P M L Q N H ->
dist6 A B II J O Q ->
A<>K -> B<>K ->
is_on_inter P II B J A ->
is_on_inter Q II A J B ->
is_on_inter O M N P Q ->
is_on_inter H II B A K ->
is_on_inter M B K J A ->
is_on_inter N A K J B ->
is_on_inter L A II K B ->
Col II J K ->
Col O A B.
Proof.
intro Hhex;intros.
geo_norm.
create_line M L lML.
create_line H N lHN.
create_line L Q lLQ.
create_line H P lHP.
create_line P M lPM.
create_line Q N lQN.
cases_line lML lHN.
solve_col.
not_eq x12 x11.
not_eq x12 x10.
not_eq lLQ x11.
not_eq x3 x11.
not_eq lLQ lHN.
not_eq lPQ lMN.
not_eq x8 x7.
collapse.
hexamy_proof P M L Q N H P Q L M N H.
Qed.