proposition: Lemma cong_preserves_bet : forall B A' A0 E D' D0, Bet B A' A0 -> Cong B A' E D' -> Cong B A0 E D0 -> Out E D' D0 -> Bet E D' D0.
proof: Proof. intros. unfold Out in H2. spliter. induction H4. assumption. assert (Le E D0 E D'). eapply l5_5_2. exists D'. split. assumption. Cong. assert(Le E D' E D0). apply (l5_6 B A' B A0); trivial. apply l5_5_2. exists A0. split. assumption. Cong. assert(Cong E D' E D0). apply le_anti_symmetry. assumption. assumption. assert(D0 = D'). eapply between_cong. apply H4. Cong. subst D'. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le