proposition: Lemma expRxDyMexpx x y : expR (x + y) * expR (- x) = expR y.
proof: Proof. set v := LHS; pattern x in v; move: @v; set f := (X in let _ := X x in _) => /=. apply: etrans (_ : f x = f 0) _; last by rewrite /f add0r oppr0 expR0 mulr1. apply: is_derive_0_is_cst => x1. apply: trigger_derive. by rewrite /GRing.scale /= mulrN1 addr0 mulr1 mulrN addrC mulrC subrr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex