proposition: Lemma least_equivalence r: reflexivep r -> sub (diagonal (substrate r)) r.
proof: Proof. by move=> rr t /diagonal_i_P [pt Ps PQ]; rewrite -pt -PQ; apply: rr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)