`(x : R) `{Lt R} `{Zero R} `{p : PropHolds (0 < x)} : 0 < x := p. (* Lemma stdlib_semiring_theory R `{SemiRing R} : Ring_theory.semi_ring_theory 0 1 (+) (.*.) (=). Proof. Qed.
Require Import Require Import