let h, k be Real; :: thesis: exp_R (h - k) = (exp_R h) / (exp_R k)
exp_R (h - k) = (exp_R h) * (exp_R (- k)) by SIN_COS:50
.= (exp_R h) * (1 / (exp_R k)) by TAYLOR_1:4
.= (exp_R h) / (exp_R k) ;
hence exp_R (h - k) = (exp_R h) / (exp_R k) ; :: thesis: verum