proposition: Lemma elevenOverTwelve_le_One : / 4 + / 3 + / 3 < 1.
proof: Proof. apply: (Rmult_lt_reg_r 3); first exact: Rplus_lt_pos. rewrite 2!mulRDl -Rinv_l_sym // mul1R mulRC. apply: (Rmult_lt_reg_r 4); first exact: Rmult_lt_0_compat. rewrite 2!mulRDl -mulRA -Rinv_l_sym //=. rewrite !(mulR1, mul1R) 2!mulRDl !mul1R. rewrite addRC; apply: Rplus_lt_compat_l. apply: Rplus_lt_compat_r; apply: (Rlt_le_trans _ _ _ (Rlt_plus_1 _)). lra. Qed.
imports: mathcomp(all_ssreflect ssralg matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext bigop_ext fdist proba entropy aep typ_seq natbin source_code