proposition: Lemma Mpos_: 0 <= M.
proof: Proof. Proof with auto with typeclass_instances. apply FLT_pos_is_pos. apply Rmult_le_pos;[idtac|exact t4pos_]. apply FLT_pos_is_pos. apply Rmult_le_pos;[idtac|exact t3pos_]. apply FLT_pos_is_pos. apply Rmult_le_pos;[exact t1pos_|exact t2pos_]. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)