proposition: Lemma proof_derive_irrelevance g1 g2 x (g1x : derivable_pt g1 x) (g2x : derivable_pt g2 x) : (forall x, g1 x = g2 x) -> derive_pt g1 x g1x = derive_pt g2 x g2x.
proof: Proof. move: g1x g2x => [l Hl] [m Hm] Hext. move: Hl Hm ; rewrite /derivable_pt_abs => Hl Hm. have g1g2 : g1 = g2 by rewrite boolp.funeqE. have ml : l = m by subst g2; exact: (uniqueness_limite g1 x). by subst m. Qed.
imports: mathcomp(all_ssreflect) mathcomp(Rstruct) Reals Lra ssrR logb Reals_ext