proposition: Lemma inj_homo_ltn_in : {in D & D', injective f} -> {in D & D', {homo f : m n / m <= n}} -> {in D & D', {homo f : m n / m < n}}.
proof: Proof. exact: inj_homo_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype) BinNat Ring