proposition: Lemma reflectl__conga : forall A B P P', A <> B -> B <> P -> ReflectL P P' A B -> CongA A B P A B P'.
proof: Proof. intros A B P P' HAB HBP HRefl. destruct HRefl as [[A' [HMid HCol]] [HPerp|Heq]]; [|subst; apply conga_refl; auto]. assert_diffs. destruct (eq_dec_points A' B). subst A'. assert_diffs. apply l11_16; auto; apply perp_per_1; [apply perp_col1 with P'|apply perp_col1 with P]; Col; Perp. destruct HMid as [HBet HCong]. destruct (l11_49 B A' P B A' P') as [HCong1 [HConga1 HConga2]]; Cong. apply l11_16; auto; apply perp_per_1, perp_left_comm, perp_col with A; Col; [apply perp_col1 with P'|apply perp_col1 with P]; Col; Perp. destruct (bet_dec A' B A) as [HBBet|HBOut]. apply l11_13 with A' A'; assumption. apply not_bet_out in HBOut; Col. assert_diffs. apply l6_6 in HBOut. apply l11_10 with A' P A' P'; trivial; apply out_trivial; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2