proposition: Lemma inf_decreasing1 r f j: order r -> fgraph f -> sub (range f) (substrate r) -> sub j (domain f) -> has_inf_graph r f -> has_inf_graph r (restr f j) -> gle r (inf_graph r f) (inf_graph r (restr f j)) .
proof: Proof. move => or fg sr sj hs1 hs2. have srr: sub (range (restr f j)) (range f) by apply: restr_range1. apply: inf_decreasing=>//; apply: sub_trans srr sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)