proposition: Lemma preorder_reflexivity r a: preorder r -> (inc a (substrate r) <-> gle r a a).
proof: Proof. move=> [g pr _]; split; first by apply: pr. rewrite/gle;move=> h; substr_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)