[ apply x
| apply not_eq_sum_field_zero ;
unfold;
- auto new
+ autobatch
| apply y
| apply lt_zero_to_le_inv_zero
].
elim daemon.
qed.
-lemma abs_x_ge_O: \forall R: real. \forall x:R. (zero R) ≤ abs R x.
+lemma abs_x_ge_O: ∀R:real.∀x:R. 0 ≤ abs ? x.
intros;
unfold abs;
unfold max;