Library AreaMethod.simplify_constructions

Require Export area_elimination_lemmas.

Theorem combine_inter_parallel : forall A B C E F X Y r,
(on_parallel_d X C A B r) ->
(inter_ll Y C X E F) ->
~ Col C A B ->
(on_inter_line_parallel Y C E F A B).
Proof.
intro.
unfold on_parallel_d, inter_ll, on_inter_line_parallel.
intros.
DecompAndAll.
repeat split;try assumption.

assert (C<>X).
unfold not;intro.
assert (parallel C X E F).
subst C.
Geometry.
intuition.
cut (parallel A B C Y).
Geometry.
eapply col_par_par.
apply H.
Geometry.
Geometry.

unfold not;intro.
assert (parallel C X E F).
assert (parallel C X A B).
Geometry.
eapply parallel_transitivity;eauto.
intuition.

Qed.

Ltac put_on_inter_line_parallel :=
  repeat match goal with
  | H:(on_parallel_d ?X ?C ?A ?B), G:(inter_ll ?Y ?C ?X ?E ?F) |- _ =>
         let T:= fresh in assert (T:=combine_inter_parallel A B C E F X Y H G);clear H G
end.