fact: Definition two_projections_increasing r r' r'' := restriction2 (two_projections (substrate r) (substrate r')(substrate r'')) (increasing_mappings r (order_product2 r' r'')) ( (increasing_mappings r r') \times (increasing_mappings r r'')).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)