proposition: Lemma col_2_par_projp2_cong : forall A A' B B' L11 L12 L21 L22, Col L11 L12 A' -> Col L11 L12 B' -> Par L11 L12 L21 L22 -> Projp A' A L21 L22 -> Projp B' B L21 L22 -> Cong A B A' B'.
proof: Proof. intros A A' B B' L11 L12 L21 L22 HColA' HColB' HPar HProjpA HProjpB. elim HPar; clear HPar; intro HPar. { elim (eq_dec_points A' B'); intro HDiffA'B'; treat_equalities; [assert (A = B) by (apply projp_id with A' L21 L22; auto); treat_equalities; Cong|]. elim (eq_dec_points A B); intro HDiffAB; treat_equalities. { assert (HCol : Col A A' B') by (apply projp2_col with L21 L22; auto). assert (HColA : Col L21 L22 A) by (apply projp_col with A'; auto). exfalso; apply HDiffA'B'; apply l6_21 with L11 L12 A A'; Col; intro; treat_equalities; apply HPar; exists A; Col. } { assert (HPara : Plg A B B' A'). { apply pars_par_plg. { apply par_strict_col2_par_strict with L11 L12; auto. apply par_strict_symmetry; apply par_strict_col2_par_strict with L21 L22; auto; [apply projp_col with A'|apply projp_col with B']; auto. } { unfold Projp in *. destruct HProjpA as [H HElim]; clear H; elim HElim; clear HElim; intro H; destruct H as [HColA HPerp1]; [|exfalso; apply HPar; exists A'; Col]. destruct HProjpB as [H HElim]; clear H; elim HElim; clear HElim; intro H; destruct H as [HColB HPerp2]; [|exfalso; apply HPar; exists B'; Col]. apply l12_9_2D with L21 L22; Perp. } } apply plg_to_parallelogram in HPara; apply plg_cong in HPara; spliter; Cong. } } { assert (A = A') by (apply eq_sym; apply col_projp_eq with L21 L22; auto; spliter; ColR). assert (B = B') by (apply eq_sym; apply col_projp_eq with L21 L22; auto; spliter; ColR). treat_equalities; Cong. } Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors