proposition: Lemma implyb_trans a b c : a ==> b -> b ==> c -> a ==> c.
proof: Proof. by case: a=>//=->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)