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