proposition: Lemma out2__conga : forall A B C A' C', Out B A' A -> Out B C' C -> CongA A B C A' B C'.
proof: Proof. intros A B C A' C' HAOut HCOut. assert_diffs. apply l11_10 with A C A C; Out. apply conga_refl;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2