proposition: Lemma or_succ_prop' r x y: total_order r -> consecutive r x y -> y = or_succ r x.
proof: Proof. move => pa pb; apply:(conseq_unique_right pa pb); apply: (or_succ_prop pa). by exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)