proposition: Lemma out_cong_cong : forall B A A0 E D D0, Out B A A0 -> Out E D D0 -> Cong B A E D -> Cong B A0 E D0 -> Cong A A0 D D0.
proof: Proof. intros. unfold Out in H. spliter. induction H4. assert (Bet E D D0). apply (cong_preserves_bet B A A0); assumption. apply cong_commutativity. eapply l4_3. apply between_symmetry. apply H4. apply between_symmetry. apply H5. Cong. Cong. assert (Bet E D0 D). apply (cong_preserves_bet B A0 A); trivial. apply l6_6. assumption. eapply l4_3;eBetween;Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le