proposition: Lemma I_ge0 (x:I) : 0 <= x∙1.
proof: Proof. by move: (x∙2)=> /andP [-> _]. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads Monoid DijkstraMonadExamples) mathcomp(all_ssreflect all_algebra reals distr) Relational(Commutativity)