proposition: Lemma restrict_lee {aT} {rT : numFieldType} (D E : set aT) (f : aT -> \bar rT) : (forall x, E x -> 0 <= f x)%E -> D `<=` E -> forall x, ((f \_ D) x <= (f \_ E) x)%E.
proof: Proof. move=> f0 ED x; rewrite /restrict; case: ifPn => [xD|xD]. by rewrite mem_set//; apply: ED; rewrite in_setE in xD. by case: ifPn => // xE; apply: f0; rewrite in_setE in xE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets fsbigop) mathcomp(functions cardinality set_interval) signed reals ereal topology normedtype sequences