proposition: Lemma inclusionC_compose x y z (Ha:sub x y)(Hb: sub y z): (inclusionC Hb) \o (inclusionC Ha) =1 inclusionC (sub_trans Ha Hb).
proof: Proof. move=> t; by apply: R_inj; rewrite 3! inclusionC_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)