proposition: Lemma rts_surjective1 r x g: restriction_to_segmentA r x g -> surjection (restriction1 g (segment r x)).
proof: Proof. move=> [p1 p2 p3 p4]. by apply: restriction1_fs. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)