fact: Definition second_partial_map2 r r' r'':= Lf (fun f=> restriction2 (second_partial_function (substrate r'') (substrate r) (substrate r') f) (substrate r) (increasing_mappings r' r'')) (increasing_mappings (order_product2 r r') r'') (increasing_mappings r (increasing_mappings_order r' r'')).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)