proposition: Lemma noid_inl_equiv_reflexive a: inc a noid_inl_sum -> noid_inl_equiv_rel a a.
proof: Proof. move/noid_inl_sumP => [ _ pb _]. have pa: gle r (Q a) (Q a) by apply:(proj32 preorder_r); rewrite substrate_r. by exists (Q a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)