proposition: Lemma rts_function1 r x g: restriction_to_segmentA r x g -> function (restriction1 g (segment r x)).
proof: Proof. move=> [p1 p2 p3 p4]; exact: (proj31 (restriction1_prop p3 p4)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)