proposition: Lemma cardinal_set_of_increasing_functions r r': total_order r -> total_order r' -> finite_set (substrate r) -> finite_set (substrate r') -> cardinal (functions_sincr r r') = binom (cardinal (substrate r')) (cardinal (substrate r)).
proof: Proof. move => ha hb hc hd. rewrite (functions_sincr_nat_prop ha hb hc hd). by rewrite card_sincreasing_nat //; apply/card_finite_setP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)