proposition: Lemma cong3_preserves_out : forall A B C A' B' C', Out A B C -> Cong_3 A B C A' B' C' -> Out A' B' C'.
proof: Proof. intros. unfold Out in *. spliter. assert(HH:=H0). unfold Cong_3 in H0. spliter. repeat split. intro. subst A'. apply cong_identity in H0. subst A. absurde. intro. subst A'. apply cong_identity in H3. subst A. absurde. induction H2. left. apply (l4_6 A B C); assumption. right. apply (l4_6 A C B). apply H2. unfold Cong_3. repeat split; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2