proposition: Lemma or_succ_prop r x: total_order r -> (exists y, consecutive r x y) -> consecutive r x (or_succ r x).
proof: Proof. move => sa sb. have pa: (exists2 y, inc y (substrate r) & consecutive r x y). move: sb => [y ya]; move: (ya) => [la _]; exists y => //; order_tac. have pb:singl_val2 (inc^~ (substrate r)) (consecutive r x). move => u v _ up _ vp; apply: (conseq_unique_right sa up vp). exact: (proj1 (select_pr pa pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)