Lines Matching refs:rewrite

151   rewrite <- (Qred_correct (T)); simpl (Qred (T)).
172     rewrite <- (Qdiv_mult_l x z). rewrite <- (Qdiv_mult_l y z).
196   rewrite Qlt_mult_by_z with (z := (p * (1 + (2#1)^(-63))^2)).
199   rewrite <- Qmult_assoc.
200   rewrite (Qmult_comm (/ (p * (1 + (2 # 1) ^ (-63)) ^ 2)) (p * (1 + (2 # 1) ^ (-63)) ^ 2)).
201   rewrite Qmult_inv_r.
202   rewrite Qmult_1_r.
209   rewrite H5.
211   rewrite Qplus_comm.
212   rewrite Qlt_move_right.
217   rewrite Qlt_mult_by_z with (z := 85070591730234615865843651857942052864 # 18446744073709551617).
233   rewrite Qlt_mult_by_z with (z := p).
236   rewrite <- Qmult_assoc.
237   rewrite (Qmult_comm (/ p) p).
238   rewrite Qmult_inv_r.
239   rewrite Qmult_1_r.
245   rewrite H5.
247   rewrite <- Qplus_assoc. rewrite <- Qplus_comm. rewrite Qlt_move_right.
250   rewrite <- Qplus_comm. rewrite Qlt_move_right.
255   rewrite Qlt_mult_by_z with (z := 85070591730234615865843651857942052864 # 18446744073709551617).