proposition: Lemma Mpos: 0 <= M.
proof: Proof. Proof with auto with typeclass_instances. apply FLX_pos_is_pos. apply Rmult_le_pos;[idtac|exact t4pos]. apply FLX_pos_is_pos. apply Rmult_le_pos;[idtac|exact t3pos]. apply FLX_pos_is_pos. apply Rmult_le_pos;[exact t1pos|exact t2pos]. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)