proposition: Lemma Exercise1_1 r (E:= substrate r) (R := fun x y => [/\ inc x E, inc y E & glt r x y]) : order r -> (exists x y, x <> y /\ related r x y) -> [/\ transitive_r R, antisymmetric_r R & ~(reflexive_rr R)].
proof: Proof. move=> or [x [y [xy rxy]]]; split => //. + move => a b c [aE bE ab] [_ cE bc]; split => //; order_tac. + move => a b [aE bE [ab nab]] [_ _ ba]; order_tac. + have sxy : R x y by hnf; rewrite /E;split => //; try substr_tac; split. by move => ref; move: (ref _ _ sxy) => [_ [_ _ [_]]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)