proposition: Lemma l11_21_b : forall A B C A' B' C', Out B A C -> Out B' A' C' -> CongA A B C A' B' C'.
proof: Proof. intros. prolong A B A0 A B. prolong C B C0 B C. prolong A' B' A1 A' B'. prolong C' B' C1 B' C'. apply l11_13 with C0 C1. apply conga_line; Between. intro. treat_equalities. unfold Out in H. spliter. absurde. unfold Out in H. spliter. auto. intro. treat_equalities. unfold Out in H0. spliter. absurde. intro. unfold Out in H0. spliter. auto. unfold Out in H. spliter. induction H10. eapply between_inner_transitivity. apply between_symmetry. apply H3. assumption. eapply outer_transitivity_between. apply between_symmetry. apply H3. assumption. auto. unfold Out in H. spliter. auto. unfold Out in H0. spliter. induction H10. eapply between_inner_transitivity. apply between_symmetry. apply H7. assumption. eapply outer_transitivity_between. apply between_symmetry. apply H7. assumption. auto. unfold Out in H0. spliter. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2