[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

seeking proof of a trivial fact

I don't find a proof of the simple fact :
b41 : lemma forall (x, y: real): x >=0 and y <= 1 
  => x * y  <= x 
Why this lemma is not trivial in PVS ?

	Sincerely yours
-- 
Michel Levy
36 rue George Sand 38400 Saint Martin d'Hères
email : Michel.Levy@imag.fr
http://www-lsr.imag.fr/users/Michel.Levy/