proposition: Lemma eq_extremum (T : eqType) (I : finType) r x0 (p1 p2 : pred I) (F1 F2 : I -> T) : p1 =1 p2 -> F1 =1 F2 -> extremum r x0 p1 F1 = extremum r x0 p2 F2.
proof: Proof. move=> eq_p eq_F; rewrite /extremum; apply/f_equal/eq_pick => x. by rewrite !inE eq_p; under eq_forallb => i do rewrite !eq_p !eq_F. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)