proposition: Lemma functions_incr_nat_prop r r': total_order r -> total_order r' -> finite_set (substrate r) -> finite_set (substrate r') -> functions_incr r r' =c functions_incr_nat (cardinal (substrate r)) (cardinal (substrate r')).
proof: Proof. move => ha hb hc hd. have is1 :=(finite_ordered_interval2 ha hc). have is2 := (finite_ordered_interval2 hb hd). by rewrite (functions_incr_inv is1 is2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)