proposition: Lemma l11_24 : forall P A B C, InAngle P A B C -> InAngle P C B A.
proof: Proof. unfold InAngle. intros. spliter. ex_and H2 X. repeat split; try assumption. exists X. split. apply between_symmetry. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2