changelog.txt

* changed:
- renamed
  + neg_RV -> opp_RV
	+ trans_min_RV -> trans_sub_RV
	+ seq.seq -> seq
- in probability/proba.v
  + split operations into sections according to their types of values:
    random_variables, zmod_random_variables, ring_random_variables,
    and real_random_variables
  + notation "X '`/' n" is changed from (1 / n%:R) to (n%:R^-1)

* added
- in probability/proba.v
  + lemma bij_RV_unif, bij_comp_RV, neg_RV_unif, trans_RV_unif

-------------------
from 0.7.7 to 0.9.0
-------------------

* changed:
- almost no stdlib anymore
  (just using Coq's reals for interval in robustmean)

* added:
- in bigop_ext.v
  + lemmas morphs_oppr, morph_mulRDr, bigmax_le_seq, bigmax_leP_seq,
           bigmax_gt0P_seq, big_union_nondisj
- in derive_ext.v
  + lemmas open_norm_subball,
           near_eq_derive, near_eq_derivable, near_eq_is_derive
- in realType_ext.v
  + lemmas wpmulr_lgt0, wpmulr_rgt0
- in ssr_ext.v
  + lemma eqW
  + setY* (symmetric difference for finite sets), notation: "A :*: B"

* removed:
- chap2 scopes, chap2.v

-------------------
from 0.7.6 to 0.7.7
-------------------

- compatibility with HB 1.8.0

-------------------
from 0.7.5 to 0.7.6
-------------------

- compatibility with MathComp 2.3.0

-------------------
from 0.7.4 to 0.7.5
-------------------

- compatibility with MathComp-Analysis 1.7.0 only

-------------------
from 0.7.3 to 0.7.4
-------------------

- minor memory optimization

-------------------
from 0.7.2 to 0.7.3
-------------------
* added:
- in ssralg_ext.v
  + lemmas mulr_regl, mulr_regr
- in realType_ext.v
  + lemmas x_x2_eq, x_x2_max, x_x2_pos, x_x2_nneg, expR1_gt2
- new file derive_ext.v
  + lemmas differentiable_{ln, Log}
  + lemmas is_derive{D, B, N, M, V, Z, X, _sum}_eq
  + lemmas is_derive1_{lnf, lnf_eq, Logf, Logf_eq, LogfM, LogfM_eq, LogfV, LogfV_eq}
  + lemmas derivable1_mono, derivable1_homo

- lemma `conv_pt_cset_is_convex` changed into a `Let`

-------------------
from 0.7.1 to 0.7.2
-------------------

- removed RinvE' and RdivE' (replaced by RinvE and RdivE in mathcomp)
- add the robust sub-directory

-------------------
from 0.7.0 to 0.7.1
-------------------

minor fix to help porting monae

-------------------
from 0.6.1 to 0.7.0
-------------------

Port to MathComp 2

-------------------
from 0.6.0 to 0.6.1
-------------------

compatibility release

-------------------
from 0.5.2 to 0.6.0
-------------------

The main change is that now the type fdist is now parameterized by R :
numDomainType.  This is the source of many changes to related lemmas
and also of a reorganization of basic files (introduction of
realType_ext.v, etc.).

- renamed
  + fsdistbindE -> fsdistbindEcond
- added
  + fsdistbindE (unconditional RHS)
  + pmulR_lgt0', pmulR_rgt0'
  + supp_fsdist_convn
- changed
  + fsdistbindEwiden (generalized)
  + fsdist_convE, fsdist_convnE (RHS slightly changed)
- removed
  + fsdist_convn (use Convn)
  + fsdist_convA (use convA0)

-------------------
from 0.5.1 to 0.5.2
-------------------
compatibility release
- generalized:
  + invRK
-------------------
-------------------
from 0.5.0 to 0.5.1
-------------------
compatibility release
-------------------
from 0.4.0 to 0.5.0
-------------------
- added:
  + finsupp_conv_subl
  + Convn_of_FSDist_join (moved from monae)
  + notation fsdist for FSDist.t
  + definition fsdist1
  + lemma leR01
  + fdistX_prod1
  + fdistX_prod_out
- renamed:
  + incl_finsupp_conv2fsdist -> finsupp_conv_subr
  + tech1 -> FSDistBindE
  + bigfcup_fset1 -> bigfcup_imfset
  + fdist_of_Dist -> fdist_of_fs
  + fdist_of_FSDistE -> fdist_of_fsE
  + fdist_of_finFSDist -> fdist_of_finfs
  + rsum_fdist_supp -> sum_fdist_supp
  + FSDist_ext -> fsdist_ext
  + FSDist_supp_neq0 -> fsdist_supp_neq0
  + FSDist1_inj -> fsdist1_inj
  + FSDistBind1f -> fsdist1bind
  + FSDistBindp1 -> fsdistbind1
  + FSDistBindA -> fsdistbindA
  + FSDistfmap -> fsdistmap
  + FSDistfmap_id -> fsdistmap_id
  + FSDistfmap_comp -> fsdistmap_comp
  + FSDistfmapE -> fsdistmapE
  + supp_FSDistfmap -> supp_fsdistmap
  + FSDistfmap1 -> fsdistmap1
  + FSDistfmap_FSDist1 -> fsdist1map
  + FSDist_finsuppD1 -> fsdist_suppD1
  + FSDistjoin -> fsdistjoin
  + FSDistjoinE -> fsdistjoinE
  + FSDistjoin1 -> fsdistjoin1
  + FSDistfmap_affine -> fsdistmap_affine
  + FSDist_scalept_conv -> fsdist_scalept_conv
  + FSDist_eval -> fsdist_eval
  + FSDist_eval_affine -> fsdist_eval_affine
  + Convn_of_FSDist -> Convn_of_fsdist
  + Convn_of_FSDist_affine -> Convn_of_fsdist_affine
  + Convn_of_FSDist_join -> Convn_of_fsdistjoin
  + Convn_of_FSDist_FSDist1 -> Convn_of_fsdist1
  + Convn_of_FSDist_FSDistfmap -> Convn_of_fsdistmap
  + FSDist1.d -> fsdist1
  + FSDist1.dE -> fsdist1E
  + FSDist1.supp -> supp_fsdist1
  + FSDistBindE -> fsdistbindEwiden
  + FSDistBind.supp -> supp_fsdistbind
  + FSDistBind.dE -> fsdistbindE
  + ConvnFSDist.d -> fsdist_convn
  + ConvnFSDist.dE -> fsdist_convnE
  + ConvFSDist.d -> fsdist_conv
  + ConvFSDist.bind_left_distr -> fsdist_conv_bind_left_distr
  + finsupp_Conv -> supp_fsdist_conv
  + ConvFSDist.convA -> fsdist_convA
  + FDist1.t -> fdist1
  + FDist1.P -> fdist1P
  + FDist1.dE1 -> fdist1E1
  + FDist1.supp -> supp_fdist1
  + FDistBind.t -> fdistbind
  + FDistBind.dE -> fdistbindE
  + FDistBind1f -> fdist1bind
  + FDistBindp -> fdistbind1
  + FDistBindA -> fdistbindA
  + FDistMap.d -> fdistmap
  + FDistMap.dE -> fdistmapE
  + FDistMap.id -> fdistmap_id
  + FDistMap.comp -> fdistmap_comp
  + Pr_FDistMap -> Pr_fdistmap
  + ConvnFDist.d -> fdist_convn
  + ConvnFDist.fdist1 -> fdist_convn1
  + ConvnFDist.cst -> fdist_convn_cst
  + ConvFDist.d -> fdist_conv
  + ConvFDist.dE -> fdist_convE
  + AddFDist.d -> fdist_add
  + AddFDist.dE -> fdist_addE
  + AddFDist_conv -> fdist_convn_add
  + DelFDist.d -> fdist_del
  + DelFDist.dE -> fdist_delE
  + DelFDist.f -> fdist_del_idx
  + DelDistConvex -> fdist_convn_del
  + D1FDist.d -> fdistD1
  + D1FDist.dE -> fdistD1E
  + D1FDist.card_fdist_supp -> card_supp_fdistD1
  + D1FDist.d_eq0 -> fdistD1_eq0
  + D1FDist.d_0 -> fdistD1_0
  + barycenter_convnfdist -> barycenter_fdist_convn
  + S1_convn_proj -> S1_Convn_proj
  + S1_convn -> S1_Convn
  + affine_function_Sum -> Convn_comp
  + eq_Convn -> eq_convn
  + convn_proj -> Convn_proj
  + ConvnFDist1 -> Convn_fdist1
  + convn1E -> ConvnI1E
  + convnE -> ConvnIE
  + convn2E -> ConvnI2E
  + convn_const -> Convn_cst
  + convn_idem -> Convn_idem
  + convn_weak -> Convn_weak
  + convnDr -> ConvnDr
  + convnDl -> ConvnDl
  + convnDlr -> ConvnDlr
  + Convn_convnfdist -> Convn_fdist_convn
  + Binary.d -> fdist_binary
  + Binary.dE -> fdist_binaryE
  + Binary.d_sum_swap -> fdist_binary_sum_swap
  + Binary.dxx -> fdist_binaryxx
  + I2FDist.t -> fdistI2
  + I2FDist.p1 -> fdistI21
  + I2FDist.p0 -> fdistI20
  + bind_left_distr -> fdist_conv_bind_left_distr
  + PermFDist.d -> fdistI_perm
  + PermFDist.dE -> fdistI_permE
  + PermFDist.dE1 -> fdistI_perm1
  + PermFDist.mul -> fdistI_permM
  + PermFDist.tperm -> fdistI_tperm
  + PermFDist.d1 -> fdistI_perm_fdist1
  + ProdFDist.d -> fdist_prod
  + ProdFDist.dE -> fdist_prodE
  + ProdFDist.fst -> fdist_prod1
  + fst_convex -> fdist_prod1_conv
  + Pr_ProdFDist -> Pr_fdist_prod
  + TupleFDist.d -> fdist_rV
  + TupleFDist.dE -> fdist_rVE
  + TupleFDist.zero0 -> fdist_rV0
  + TupleFDist.S -> fdist_rVS
  + TupleFDist.one -> fdist_rV1
  + TupleFDist.to_bivar -> fdist_prod_of_fdist_rVw
  + TupleFDist.head_of -> head_of_fdist_rV_fdist_rV
  + TupleFDist.tail_of -> tail_of_fdist_rV_fdist_rV
  + Pr_FDistMap_RV2 -> Pr_fdistmap_RV2
  + CondFDist.d -> fdist_cond
  + CondFDist.dE -> fdist_condE
  + CondFDist.Pr -> Pr_fdist_cond
  + Bivar.fst -> fdist_fst
  + Bivar.fstE -> fdist_fstE
  + Bivar.dom_by_fst -> dom_by_fdist_fst
  + Bivar.dom_by_fstN -> dom_by_fdist_fstN
  + Bivar.snd -> fdist_snd
  + Bivar.sndE -> fdist_sndE
  + Bivar.dom_by_snd -> dom_by_fdist_snd
  + Bivar.dom_by_sndN -> dom_by_fdist_sndN
  + Pr_Bivarfst -> Pr_fdist_fst
  + Pr_Bivarsnd -> Pr_fdist_fst
  + Uniform.d -> fdist_uniform
  + Uniform.dE -> fdist_uniformE
  + Uniform.neq0 -> fdist_uniform_neq0
  + UniformSupport.d -> fdist_uniform_supp
  + UniformSupport.dET -> fdist_uniform_supp_in
  + UniformSupport.dEN -> fdist_uniform_supp_notin
  + UniformSupport.restrict -> fdist_uniform_supp_restrict
  + UniformSupport.big_distrr -> fdist_uniform_supp_distrr
  + UniformSupport.neq0 -> fdist_uniform_supp_neq0
  + BinarySupport.a -> fdist_binary_supp0
  + BinarySupport.b -> fdist_binary_supp1
  + BinarySupport.enum_fdist_supp -> enum_fdist_binary_supp
  + BinarySupport.rsumE -> enum_fdist_binary_supp
  + CondJFDist0.d -> jfdist_cond0
  + CondJFDist0.dE -> jfdist_cond0E
  + CondJFDist.d -> jfdist_cond
  + CondJFDist.dE -> jfdist_condE
  + CondJFDist.dNE -> jfdist_cond_dflt
  + CJFDist.t -> jfdist_prod0
  + CJFDist.joint_of -> jfdist_prod
  + CJFDist.CondJFDistE -> fdist_cond_prod
  + CJFDist.E -> jcPr_fdistX_prod
  + CJFDist.split -> fdist_split
  + CJFDist.splitE -> fdist_prodK
  + Multivar.to_bivar -> fdist_prod_of_rV
  + Multivar.to_bivarE -> fdist_prod_of_rVE
  + Multivar.belast_last -> fdist_belast_last_of_rV
  + Multivar.belast_lastE -> fdist_belast_last_of_rVE
  + Multivar.from_bivar -> fdist_rV_of_prod
  + Multivar.from_bivarE -> fdist_rV_of_prodE
  + Multivar.from_bivarK -> fdist_prod_of_rVK
  + Multivar.to_bivarR -> fdist_rV_of_prodK
  + Multivar.head_of -> head_of_fdist_rV
  + Multivar.tail_of -> tail_of_fdist_rV
  + Pr_Multivar -> Pr_fdist_prod_of_rV
  + Pr_Multivar1 -> Pr_fdist_prod_of1
  + Pr_Multivar2 -> Pr_fdist_prod_of2
  + cast_RV_tupledist1 -> cast_RV_fdist_rV1
  + cast_rV1_RV_tupledist1 -> cast_RV_fdist_rV10
  + cast_rV1_fun_rV1 -> cast_fun_rV10
  + E_cast_RV_tuplefdist1 -> E_cast_RV_fdist_rV1
  + Var_cast_RV_tuplefdist1 -> Var_cast_RV_fdist_rV1
  + head_of_fst_belast_last -> head_of_fdist_rV_belast_last
  + entropy_from_bivar -> entropy_fdist_rV_of_prod
  + Pr_FDistMap_r -> jcPr_fdistmap_r
  + Pr_FDistMap_l -> jcPr_fdistmap_l
  + Swap.d -> jfdistX
  + Swap.fst -> jfdistX1
  + Swap.snd -> jfdistX2
  + Swap.Pr -> Pr_jfdistX
  + Swap.dI -> jfdistXI
  + Swap.ProdFDist -> jfdistX_prod
  + Swap.dom_by -> jfdistX_dom_by
  + Swap_RV2 -> fdistX_RV2
  + Nth.d -> fdist_nth
  + Nth.dE -> fdist_nthE
  + Nth.head_ofE -> head_of_fdist_rV_fdist_nth
  + MargDist.d -> fdist_col'
  + MargDist.dE -> fdist_col'E
  + MargDist.tail_ofE -> tail_of_fdist_rV_fdist_col'
  + Take.d -> fdist_take
  + Take.dE -> fdist_takeE
  + Take.all -> fdist_take_all
  + take_nth -> fdist_take_nth
  + PairNth.d -> fdist_prod_nth
  + PairNth.dE -> fdist_prod_nthE
  + PairTake.d -> fdist_prod_take
  + TripA.d -> fdistA
  + TripA.dE -> fdistAE
  + TripA.domin -> fdistA_domin
  + TripA.dominN -> fdistA_dominN
  + TripA.fst -> fdistA1
  + TripA.fst_snd -> fdistA21
  + TripA.snd_snd -> fdistA22
  + TripA.snd_swap -> fdistAX2
  + TtipA.snd_fst_swap -> fdistAX12
  + TripA.imset -> imsetA
  + TripA.Pr -> Pr_fdistA
  + TripA.f -> prodA
  + TripA.inj_f -> prodA_inj
  + TripA_RV3 -> fdistA_RV3
  + TripC12.d -> fdistC12
  + TripC12.dE -> fdistC12E
  + TripC12.fst -> fdistC12_fst
  + TripC12.snd -> fdistC12_snd
  + TripC12.fstA -> fdistA_C12_fst
  + TripC12.dI -> fdistC12I
  + TripC12.Pr -> Pr_fdistC12
  + jcPr_TripA_TripC12 -> jcPr_fdistA_C12
  + TripC12_RV3 -> fdistC12_RV3
  + TripAC.d -> fdistAC
  + TripAC.f -> prodAC
  + TripAC.inj_f -> inj_prodAC
  + TripAC.snd -> fdistAC2
  + TripAC.fstA -> fdistA_AC_fst
  + TripAC.fst_fst -> fdistAC_fst_fst
  + TripAC.sndA -> fdistA_AC_snd
  + TripAC.imset -> imsetAC
  + TripAC.Pr -> Pr_fdistAC
  + jcPr_TripA_TripAC -> jcPr_fdistA_AC
  + h1TripAC -> h1_fdistAC
  + hTripAC -> h_fdistA
  + TripC13.d -> fdistC13
  + TripC13.dE -> fdistC13E
  + TripC13.fst -> fdistC13_fst
  + TripC13.snd -> fdistC13_snd
  + TripC13.fst_fst -> fdistC13_fst_fst
  + TripC13.sndA -> fdistA_C13_snd
  + Proj13.d -> fdist_proj13
  + Proj13.dE -> fdist_proj13E
  + Proj13.domin -> fdist_proj13_domin
  + Proj13.dominN -> fdist_proj13_dominN
  + Proj13.snd -> fdist_proj13_snd
  + Proj13.fst -> fdist_proj13_fst
  + Proj13_TripAC -> fdist_proj13_AC
  + Proj13_RV3 -> fdist_proj13_RV3
  + Proj23.d -> fdist_proj23
  + Proj23.dE -> fdist_proj23E
  + Proj23.domin -> fdist_proj23_domin
  + Proj23.dominN -> fdist_proj23_dominN
  + Proj23.fst -> fdist_proj23_fst
  + Proj23.snd -> fdist_proj23_snd
  + Proj23.Pr -> Pr_fdist_proj23_domin
  + Self.d -> fdist_self
  + Self.dE -> fdist_selfE
  + Self.fst -> fdist_self1
  + Self.swap -> fdistX_self
  + MultivarPerm.d -> fdist_perm
  + MultivarPerm.dE -> fdist_permE
  + TakeDrop.d -> fdist_take_drop
  + scalept_rsum -> scalept_sum
  + Rnneg -> Rnng
  + big_scalept -> big_morph_scalept
  + scaled_pt -> scaled
  + sum_of_scaled_pt -> sum_of_scaled
  + scaled_pt_of_sum -> scaled_of_sum
  + sum_of_scaled_ptK -> sum_of_scaledK
  + scalept0 -> scale0pt
  + scalept1 -> scale1pt
  + scalept_comp -> scaleptA
  + scalept_addpt -> scaleptDr
  + scalept_addR -> scaleptDl
  + weight_bary -> weight_barycenter
  + S1_conv -> affine_S1
  + scalept_bary -> scalept_barycenter
  + barycenter_big_fin -> barycenter_map
  + barycenter_perm -> ssum_perm
  + barycenter_fdist_convn -> ssum_fdist_convn
  + `d_ -> `p_
  + JointEntropy.h -> joint_entropy
  + JointEntropy.entropyE -> entropy_rV
  + CondEntropy.h1 -> cond_entropy1
  + CondEntropy.h -> cond_entropy
  + MutualInfo.mi -> mutual_info
  + sum_parti_finType -> partition_big_fin_img
  + big_singl_rV -> big_rV1_ord0
  + R_convex_function_atN' -> RNconvex_function_at
  + R_concave_function_atN' -> RNconcave_function_at
  + R_convex_functionN' -> RNconvex_function
  + R_concave_functionN' -> RNconcave_functionN
  + OutFDist.d -> fdist_out
  + OutFDist.dE -> fdist_outE
  + tuple_pmf_out_fdist -> fdist_rV_out
  + MutualInfoChan.mut_info ->  mutual_info_chan
  + mut_info_chanE -> mutual_info_chanE
  + jcPr_max -> jcPr_le1
  + CondEntropyChan.h -> cond_entropy_chan
  + CondEntropyChanE -> cond_entropy_chanE
  + CondEntropyChanE2 -> cond_entropy_chanE2
  + Receivable.t -> receivable
  + Receivable.def -> receivable_prop
  + Receivable.mk -> mkReceivable
  + receivableE -> receivable_propE
  + not_receivable_uniformE -> not_receivable_prop_uniform
  + PosteriorProbability.d -> fdist_post_prob
  + PosteriorProbability.dE -> fdist_post_probE
  + PosteriorProbability.ppE -> post_probE
  + PosteriorProbability.Kppu -> post_prob_uniform_cst
  + MarginalPostProbability.d -> fdist_marginal_post_prob
- Removed:
  + Module TripA'
  + imset_fst
  + big_scalept
  + `p_
  + big_rV_0
  + CJFDist.make_joint
  + JointFDistChan.d
  + `J(P, W) notation
- changed:
  + scaledptR0 (now derived from the interface of quasi real cones)
    and renamed scalept0

-------------------
from 0.3.8 to 0.4.0
-------------------
- packed classes (affine, biglub, convex, concave) redefined with HB
- added:
  + notation {Biglub_morph T -> R}
- renamed:
  + SemiCompleteSemiLattice -> SemiCompSemiLatt
  + idfun_is_biglub_affine -> idfun_is_biglubmorph
  + comp_is_biglub_affine -> comp_is_biglubmorph
  + affineP -> affine_functionP

-------------------
from 0.3.7 to 0.3.8
-------------------
compatibility release

-------------------
from 0.3.6 to 0.3.7
-------------------
compatibility release

-------------------
from 0.3.5 to 0.3.6
-------------------
compatibility release

-------------------
from 0.3.4 to 0.3.5
-------------------

* added
- in ssrR.v
  + lemma invR_ge0
- in ssrZ.v
  + lemmas addZAC, addZCA, neq_Zlt
* renamed:
- in ssrR.v
  + subr_le0 -> subR_le0
- in reals_ext.v
  + pos_ffun -> nneg_finfun
  + pos_ff_ge0 -> nneg_finfun_ge0
  + pos_fun -> nneg_fun
* changed:
- row_nth moved and renamed to bitseq_row_nth
* removed:
  + sumR_setT (use finset.big_set in MathComp)
  + eq_imagel (use classical_sets.eq_imagel in MathComp-Analysis)
  + eq_bigcup (use classical_sets.eq_bigcup in MathComp-Analysis)

-------------------
from 0.3.3 to 0.3.4
-------------------

* added:
- in ssrZ.v
  + lemmas ltZ_addl, ltZ_addr, pmulZ_rgt0
  + lemmas intRD, leZ0n
- in ssrR.v
  + lemmas expRn_gt0, ltR0n_neq0, lt0Rn_neq0', eqR_divl_mulr
- in proba.v
  + lemmas scalel_RVA, scaler_RVA, sq_RV_pow2, sq_RV_ge0, E_trans_min_RV
  + lemma Pr_lt1

* renamed:
- in necset.v
  + lemma nesetU_bigsetU -> nesetU_bigcup

* changed:
- in ssr_ext.v
  + remove eq_tcast in favor of eq_tcast2 (renamed to eq_tcast)
- in aep.v
  + a cleaner expression for aep_sigma2
- in proba.v
  + stopped importing the unused Nsatz
- in Rbigop.v
  + generalize leR_sumR

* removed:
- in convex.v:
  + definition choice_of_Object
- in aep.v:
  + lemma E_mlog (since it is equivalent to entropy.entropy_Ex)

-------------------
from 0.3.2 to 0.3.3
-------------------

* removed:

- in ldpc_algo_proof.v:
  + lemma sumn_eq0P

-------------------
from 0.3.1 to 0.3.2
-------------------

* added:

- in Reals_ext.v:
  + lemmas onem_le, onem_lt
  + module OProb for inferring values in the open unit interval
    * notation %:opr
    * technical lemmas oprob_gt0, oprobK, oprob_pdivRnnm, oprob_add_gt0, etc.
    * a canonical instance for the cplt and the multiplication of two oprob's
  + a canonical instance of Rpos for oprob
  + lemmas onem_prob, onem_oprob
  + lemmas prob_trichotomy and prob_trichotomy'
- in ssrR.v:
  + lemma ltR_subr_addr
- in convex.v:
  + lemmas convA'_oprob, convACA'
- in fdist.v:
  + technical lemmas about oprob and s_of, r_of, p_of, q_of
    * with canonical instances
- in necset.v:
  + lemmas conv_in_conv_pt_set, conv_in_conv_set, convA_pt_set, etc.
  + lemma affine_image_conv_set
  + lemma conv_pt_cset_is_convex, canonical conv_pt_cset,
    lemma conv_pt_cset, canonical conv_cset,
    lemma oplus_conv_cset_is_convex, canonical oplus_conv_cset
  + lemma conv_set1
- in classical_sets_ext.v:
  + lemma set1_inj

* changed:
  + modify the convex space structure on (convex_set _) to reuse conv_set instead of
    differently defining another convex combination operation
  + move and rename convex.{Rpos_prob_Op1, Rpos_prob, Rpos_probC}
    to Reals_ext.{prob_divRposxxy, divRposxxy, divRposxxyC}.

* moved:
  + lemma onem_div from convex.v to Reals_ext.v

-----------------
from 0.3 to 0.3.1
-----------------

- added:
  + Notations [affine of f] and [affine of f as g]
  + Notation biglub_morph
  + lemmas prob_ge0, prob_le1 (also as Hint Resolve)
  + views leR2P and ltR2P
  + constructor Prob.mk to build prob from boolean inequalities and
    Prob.mk_ to build prob from Prop inequalities
  + definition prob_invp, lemma Prob_invp
  + lemmas prob_gt0', prob_lt1', probmul_eq1
- renamed:
  + Module AffineFunction -> Affine
  + Notation AffineFunction -> Affine
  + Notation affine_function -> affine
  + affine_functionP' -> affine_conv
  + CSet.Class -> CSet.Mixin
- changed:
  + affine_function_id_proof/affine_function_id ->
      idfun_is_affine/Canonical idfun_affine
  + affine_function_comp_proof'/affine_function_comp_proof/affine_function_comp ->
      comp_is_affine/Canonical comp_affine
  + in Section with_affine_projection and Section S1_proj_Convn_finType
    * prj/prj_affine -> prj : {affine ... -> ...}
  + Convn_of_FSDist_FSDistfmap -> to use {affine ...}
  + biglub_morph, biglub_lub_morp -> to use {Biglub_morph ...}
  + multiple inheritance in Module BiglubMorph
  + biglub_affine_id_proof -> idfun_is_biglub_affine/Canonical idfun_is_biglub_affine
  + biglub_affine_comp_proof -> comp_is_biglub_affine/Canonical comp_biglub_affine
  + proof field of Prob.t now in bool
  + prob_subType declaration for Prob.t
  + generalize binary_symmetric_channel.closed to ssrR.ltR2W
- moved:
  + lemma Rpos_prob_Op1, Rpos_prob, Rpos_probC, onem_div from convex.v to Reals_ext.v
- removed:
  + affine_function_at
  + image_preserves_convex_hull', is_convex_set_image'
  + lemma Prob.ge0
  + lemma prob_ext
  + lemmas eqprob, eqprobP

-----------------
from 0.2.2 to 0.3
-----------------

- moved:
  + from convex_choice.v to fsdist.v
    * FSDist_convType
    * convn_convnfsdist
    * fsdist_orderedConvMixin
  + from necset.v to fsdist.v
    * finsupp_Conv
    * FSDist_eval_affine
    * FSDist_scalept_conv
    * Convn_of_FSDist
    * Convn_of_FSDist_affine
    * Convn_of_FSDist_FSDist1
    * Convn_of_FSDist_FSDistfmap
    * triangular_laws_left0
  + row_of_tuple_inj from types.v to ssralg_ext
  + derive_sincreasing_interv moved to Ranalysis_ext.v
  + num_occ_flatten from string_entropy.v to num_occ.v
- renamed:
  + lub_op -> biglub
  + lub_op1 -> biglub1
  + lub_op_bigsetU -> biglub_bignesetU
  + lub_op_bigcup -> biglub_bigcup
  + lub_op_setU -> biglub_setU
  + lub_of_flatten -> biglub_flatten
  + lub_binary -> lub
  + lub_binaryC -> lubC
  + lub_binaryA -> lubA
  + lub_binaryxx -> lubxx
  + lub_binaryAC -> lubAC
  + lub_binaryCA -> lubCA
  + lub_binaryACA -> lubACA
  + lub_binaryKU -> lubKU
  + lub_binaryUK -> lubUK
  + lub_binaryKUC -> lubKUC
  + lub_binaryUKC -> lubUKC
  + lub_binaryD{r,l} -> lubD{r,l}
  + lub_op_morph -> biglub_morph
  + lub_lub_binary_morph -> biglub_lub_morph
  + LubOpMorph -> BiglubMorph
  + LubOpAffine -> BiglubAffine
  + lub_op_affine_id_proof -> biglub_affine_id_proof
  + lub_op_affine_comp_proof -> biglub_affine_comp_proof
  + lub_opD{r,l} -> biglubD{r,l}
  + lub_op_conv_pt_setE -> biglub_conv_pt_setE
  + lub_op_conv_pt_setD -> biglub_conv_pt_setD
  + lub_op_conv_set -> biglub_conv_setE
  + lub_op_conv_setD -> biglub_conv_setD
  + lub_op_iter_conv_set -> biglub_iter_conv_set
  + lub_op_hull -> biglub_hull
- changed:
  + setU_bigsetU in necset.v changed to bigcupsetU2E in classical_sets.v
  + MVT_cor1_pderivable_new in ln_facts changed to MVT_cor1_pderivable_closed_continuity
    and moved to Ranalysis_ext.v
  + MVT_cor1_pderivable_new_var in ln_facts.v changed to MVT_cor1_pderivable_open_continuity
    and moved to Ranalysis_ext.v
  + sum_num_occ renamed to sum_num_occ_size from and moved from string_entropy.v to num_occ.v
  + in ssrR.v, gtR_eqF, ltR_eqF, invRK, invRM have now hypotheses in bool instead of Prop
  + in ssrR.v, oppR_lt0 and oppR_gt0 are now equivalences
- renamed:
  + derive_increasing_interv_ax_left -> pderive_increasing_ax_open_closed
  + derive_increasing_interv_ax_right -> pderive_increasing_ax_closed_open
  + derive_increasing_interv_left -> pderive_increasing_open_closed
  + derive_increasing_interv_right -> pderive_increasing_closed_open
  + derive_increasing_ad_hoc -> pderive_ad_hoc
  + ltr_subl_addl -> ltR_subl_addl
  + convex_choice.v -> convex.v
- removed:
  + from ssrR.v:
    * Reqb, eqRP, R_eqMixin, R_eqType, R_choiceType, ROrder.orderMixin,
      R_porderType, R_latticeType, R_distrLatticeType, R_orderType

-----------------
from 0.2 to 0.2.1
-----------------

- changed:
  + in ssrZ.v:
    * Z_of_nat_le -> leZ_nat, Z_of_nat_lt -> ltZ_nat
    * Z<=nat -> %:Z
- renamed:
  + in classical_sets_ext.v: 
    image_subset -> subset_image
- removed:
  + in classical_sets_ext.v:
    set1_inj
    fullimage_subset

-----------------
from 0.1.2 to 0.2
-----------------

warning: this changelog entry is not exhaustive

- renamed:
  + in Rbigop.v:
    * rsumr_ge0 -> sumR_ge0, rsumr_gt0 -> sumR_gt0
    * ler_rsum_support -> leR_sumR_support,ler_rsum -> leR_sumR, ler_rsum_l -> leR_sumRl,
      ler_rsum_l_support -> leR_sumRl_support, ltr_rsum_support -> ltR_sumR_support,
      ltr_rsum -> ltR_sumR
    * rsum_setT -> sumR_setT, rsum_ord_setT -> sumR_ord_setT
    * prsumr_seq_eq0P -> psumR_seq_eq0P, prsumr_eq0P -> psumR_eq0P
    * ler_rsum_Rabs -> leR_sumR_Rabs, ler_rsum_predU-> leR_sumR_predU
    * classify_big -> classify_sumR
    * Rle_big_eq -> leR_sumR_eq
    * sum_f_R0_rsum -> sum_f_R0_sumR
    * bigmul_eq0 -> rprod_eq0
    * rprodr_gt0 -> prodR_gt0, rprodr_ge0 -> prodR_ge0, rprodr_gt0_inv-> prodR_gt0_inv, rprodr_ge1 -> prodR_ge1
    * ler_rprod -> leR_prodR
    * log_rmul_rsum_mlog -> log_prodR_sumR_mlog
    * Rle_bigRmax -> leR_bigmaxR, Rle_0_bigRmax -> bigmaxR_ge0
    * bigrmax_undup -> bigmaxR_undup, bigrmax_cat -> bigmaxR_cat, bigrmax_perm -> bigmaxR_perm, bigrmax_eqi -> bigmaxR_eqi
    * rmax_imset -> bigmaxR_imset, rmax_imset' -> bigmaxR_imset_helper
    * Rle_bigrmax_R -> leR_bigmaxRl
    * bigrmax_max_seq -> bigmaxR_seq_eq, bigrmax_max - bigmaxR_eq
    * rmax_distrr -> bigmaxR_distrr, rmax_distrl -> bigmaxR_distrl
    * bigminn_min -> leq_bigmin, big_rmax_bigminn -> bigmaxR_bigmin, big_rmax_bigminn_vec -> bigmaxR_bigmin_vec
    * bigmul_constE -> prodR_constE, bigmul_card_constE -> prodR_card_constE, bigmul_m1pow -> prodRN
    * E_sumr -> E_sumR
    * unit_RV1 -> pr_eq_unit
    * Pr_domin_fst -> Pr_domain_setX
  + \Pr[ X = a ] -> `Pr[ X = a ], \Pr[ X >= a ] -> `Pr[ X >= a ]
  + RVar.d -> dist_of_RV
  + RVar.dE -> pr_eqE', RVar.Pr_Set -> pr_inE'
  + RVar.Pr -> RVarPr
  + p_of -> ambient_dist
  + cPr -> jcPr
  + cPr0 -> cPr
  + cPr0_Pr -> cPrET
  + cPr0_set0 - cPrE0
  + PrX_setT -> Pr_XsetT
  + bayes -> jBayes
  + law_of_total_probability -> total_prob, total_prob -> jtotal_prob_cond
  + product_rule -> jproduct_rule_cond, product_rule0 -> jproduct_rule
  + inde_drv -> inde_rv (in proba.v), cinde_drv -> jcinde_rv (in cinde.v)
  + RV_Pr_C -> pr_eq_pairC, RV_Pr_C_set -> pr_in_pairC
  + RV_Pr_A -> pr_eq_pairA, RV_Pr_A_set -> pr_in_pairA
  + RV_Pr_AC -> pr_eq_pairAC, RV_Pr_AC_set -> pr_in_pairAC
  + RV_Pr_comp_set -> pr_in_comp, RV_Pr_comp -> pr_eq_comp
  + reasoning_by_cases -> jcreasoning_by_cases
- added:
  + divRBl in ssrR.v
  + notation `d_ for RVar.d
  + notation `o for comp_RV
  + sumR_neq0
  + bigcup_set1
  + simple technical lemmas to deal with `*T, T*`, and `* (setX)
  + Pr_setTX
  + CondFDist in proba.v
  + lemmas about cPr proba.v (cPrE0, Pr_cPr_gt0, cPr_cplt, product_rule, cPr_diff, cPr_union_eq)
  + Pr_Bivarfst, Pr_Bivarsnd, Pr_Multivar, Pr_Multivar{1,2}
  + conditional version of random variables and independence in proba.v
  + pr_eq_pairCA, pr_in_pairCA
  + cpr_in_Eset1, cpr_in_set1F
  + reasoning_by_cases, creasoning_by_cases
  + cpr_in_pair* lemmas in proba.v
  + cinde.v -> graphoid.v
- changed:
  + generalize pr_geq to any porderType
  + definition of notation @^-1 now uses preim instead of finset notations
  + capacity changed from a relation to a definition using Rstruct.real_sup
  + slight generalization of bigcup_setX, bigcup_set0
  + slight generalization of RV_Pr_setXunit (renamed pr_eq_pair_setT)
- removed:
  + notations `E_, `V_
  + duplicate of E_leng_cw
  + PrX_diff, PrX_union
  + Pr_RV2C
  + RV_Pr_CA, RV_Pr_CA_set
  + Pr_domin_snd
  + RVarPr
  + most marginal_* lemmas and technical lemmas from cinde.v
  + RV_Pr_lC, etc., RV2_Pr*congr* lemmas, from cinde.v

---------------------
from 0.1.1 to 0.1.2 :
---------------------

- moved:
  + subR_onem from necset.v to Reals_ext.v
  + from necset.v to fsdist.v
    * bigfcup_fset1
    * fbig_pred1_inj
    * FSDistfmap_FSDist1
    * FSDist_finsuppD1
    * FSDist_prob
  + set1_inj from necset.v to classical_sets_ext.v

-------------------
from 0.1 to 0.1.1 :
-------------------

added:
- order canonical structures in ssrR.v
renamings:
- imageA -> image_comp (deprecated)
- image_idfun -> image_id (deprecated)
- bigcup0 -> bigcup_set0
- bigcup1 -> bigcup_set1
- bigcup_set1 -> bigcup_of_singletons
- bigcup_const -> bigcup_of_const
- altConvType -> naryConvType
added:
- <&>_ notation for the operator of naryContType
  + _ <& _ &> _ for its binary version
removed:
- Lemma to_bivar_entropy (redundant with entropy_to_bivar)
- file arg_rmax.v
replaced:
- custom arg_rmax with new order.v's [arg max_(i > i0) F]%O

-------------------
from 0.0.7 to 0.1 :
-------------------

new lemmas:
- FSDist.le1
new type:
- altConvType, together with equivalence proofs of several axiomatics
renamings:
- Joet -> lub_op
- joet -> lub_binary
- Convn_indexed_over_finType -> Convn_finType
notations:
- <$>_ for Convn__finType (on the model of <|>_)
- |_| fr lub_op (still [+] for lub_binary)
- _ <| _ |> _ lowered to level 49
- << and <<b changed to `<< and `<<b (level change)

---------------------
from 0.0.6 to 0.0.7 :
---------------------

renamings:
- Module jtype -> Module JType
  + jtype.jtype -> JType.t
  + jtype.mkJtype -> JType.mk
  + jtype.f -> JType.f
  + etc.
- MultivarPerm.entropy -> entropy_multivarperm
- head_of_nth0 -> Nth.head_ofE
- MargFDist.zero -> MargFDist.tail_ofE
- ide_swap -> swapK
notation changes:
- notation \Conv_ -> <|>_
- `NE -> %:ne (prefix to postfix)
- `Rpos -> %:pos
- `Rnneg -> %:nng
- `Pr -> %:pr
new notation:
- E `* F for setX E F
lemmas:
- (bij_inj bij_swap) instead of inj_swap 
files:
- fdist.v split into fdist.v (distributions) and proba.v (probabilities)

--------------------
from 0.0.5 to 0.0.6:
--------------------

renamings:
- Pr_big_union_disj -> Boole_eq (generalization)
- setX1' -> setX1r (direction change)
- setX0 -> setX0r
- Int_part_pos -> Int_part_ge0
- CFDist -> CJFDist
- CondFDist -> CondJFDist0
- CondFDistT -> CondJFDist
- scha moved from success_decode_bound.v to channel_code.v
new notation:
- P `(| a ) for CondFDistT.d
files:
- pinsker_fun.v has been integrated into pinsker.v
- proba.v renamed to fdist.v (proba.v kept for compatibility)
- cproba.v renamed to jfdist.v