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