proposition: Lemma segment_injective r : total_order r -> {inc (substrate r) &, injective (segment r) }.
proof: Proof. move=> tor x y xsr ysr sxy. have p1: (sub (segment r x)(segment r y)) by rewrite sxy. have p2: (sub (segment r y)(segment r x)) by rewrite sxy. have p3:= (segment_monotone1 tor xsr ysr p1). have p4:= (segment_monotone1 tor ysr xsr p2). move: tor=> [or _]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)