proposition: Lemma square_nonneg : forall a, 0 <= a * a.
proof: Proof. intro a. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonneg_l; order. Qed.
imports: NZAxioms NZAddOrder