proposition: Lemma Val_a_b (a b : R) : fab a b 1 = 2 -> Derive (fab a b) 1 = 0 -> a = 2 /\ b = 2.
proof: Proof. move => Hf Hdf. rewrite /fab in Hf. rewrite ln_1 in Hf. rewrite Rdiv_1 in Hf. rewrite Rmult_0_r in Hf. rewrite Rplus_0_r in Hf. rewrite Hf in Hdf |- * => {a Hf}. split. reflexivity. replace (Derive (fab 2 b) 1) with (((b - 2) - b * ln 1) / 1 ^ 2) in Hdf. rewrite ln_1 /= in Hdf. field_simplify in Hdf. rewrite ?Rdiv_1 in Hdf. by apply Rminus_diag_uniq. apply sym_eq, is_derive_unique. apply Dfab. by apply Rlt_0_1. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)