proposition: Lemma segment_reverse : forall A B C, Bet A B C -> exists B', Bet A B' C /\ Cong C B' A B.
proof: Proof. intros. destruct (eq_dec_points A B). subst B; exists C; finish. destruct (segment_construction_3 C A A B) as [B' []]; auto. intro; treat_equalities; auto. exists B'; split; trivial. apply between_symmetry, (cong_preserves_bet A B C); Cong. apply l6_6; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le