proposition: Lemma inclusionC_fi a b (H: sub a b): injectiveC (inclusionC H).
proof: Proof. move => x y si; apply: R_inj. by rewrite - (inclusionC_pr H x) si (inclusionC_pr H y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)