proposition: Lemma l11_44_1_a : forall A B C, A <> B -> A <> C -> Cong B A B C -> CongA B A C B C A.
proof: Proof. intros. destruct (midpoint_existence A C) as [P HP]. assert_diffs. assert(CongA B A P B C P) by (apply cong3_conga; auto; repeat split; Cong). apply l11_10 with B P B P; Out. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2