proposition: Theorem Rtimes_square_nonneg : forall n : R, 0 <= n * n.
proof: Proof. intro n; destruct (Rlt_trichotomy 0 n) as [H | [H | H]]. - le_less; now apply Rtimes_pos_pos. - rewrite <- H, Rtimes_0_l; le_equal. - le_less; now apply Rtimes_neg_neg. Qed.
imports: Setoid Ring