proposition: Lemma conseq_unique_right r x y y': total_order r -> consecutive r x y -> consecutive r x y' -> y = y'.
proof: Proof. move => [or tor] [ha hb] [hc hd]. ex_middle neq. have ysr: inc y (substrate r) by order_tac. have ysr': inc y' (substrate r) by order_tac. case: (tor _ _ ysr ysr') => le1; first by case (hd _ ysr). case: (hb _ ysr'); split => //; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)