proposition: Lemma I_le1 (x:I) : x∙1 <= 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)