Add def eq_dec.

Finite_family:
Add eq_decF.

Binary_relation:
Use new API from logic_compl (br_not, eq_dec).
Rename connected <-> connected_alt,
       connected_alt_contra -> connected_contra,
       conn_equiv -> conn_equiv_alt,
       lex_conn -> lex_conn_alt,
       colex_conn -> colex_conn_alt.
Add lex_conn, colex_conn.

Monoid_compl:
Use new API from logic_compl (eq_dec).
Use new API from Binary_relation (connected*).
Rename graded_conn -> graded_conn_alt.
Add graded_conn.

Finite_dim_R:
Needs full qualification since there is a new one hiding it...

Mv stuff around.
Got rid of classic_dec (assume the type is eqType instead).

from Algebra/Monoid_compl to Compl/Binary_relation.

Rm wrong transitive_incomparability.
Add comparable, incomparable, comp_sym, incomp_sym,
    trans_incomp_compl.
Replace transitive_incomparability R -> transitive (incomparable R).
Rename trans_inc_conv -> trans_incomp_conv.

       antisym_compl <-> asym_compl,
       monomial_order -> monomial_order_incr,
       monomial_order_equiv_sto -> monomial_order_incr_equiv_sto,
       monomial_order_conv -> monomial_order_incr_conv,
       graded_monomial_order -> graded_monomial_order_incr.
Modify trans_compl.
Remove meaningless monomial_order_br_monoid_compat_min.
Add transitive_incomparability, strict_weak_order,
    trans_inc_equiv, strict_weak_order_equiv_{spo,no_asym,no_irrefl},
    conv_fix_equiv, compl_conv_eq,
    trans_inc_conv, trans_inc_compl,
    monomial_order, monomial_order_equiv_sto, monomial_order_conv,
    graded_monomial_order.

    {,total}preorder_conv_equiv,
    {,strict_}{partial,total}_order_conv_equiv,
    {refl,irrefl,sym}_compl.
WIP: {antisym,asym,trans,conn,str_conn}_compl.

Modify monomial_order, monomial_order_equiv_sto, monomial_order_conv,
       {symlex,revlex}_monomial_order,
Add bin_rel_monoid_compat_{min,max}, monomial_order_decr,
    monomial_order_decr_equiv_sto, monomial_order_br_monoid_compat_min,
    bin_rel_monoid_compat_{min,max}_conv, monomial_order_decr_conv,
    {lex,colex,symlex,revlex}_br_monoid_compat_{min,max},
    graded_br_monoid_compat_{min,max}, graded_monomial_order_decr.

Add modus_ponens_and3.

Monoid_compl:
Add graded_{irrefl,trans,conn},
    graded_{strict_partial_order,strict_total_order},
    graded_{br_plus_compat_{l,r},zero_is_{min,max}},
    graded_{br_monoid_compat_{l,r},monomial_order}.
WIP: graded_zero_is_bound is False!
TODO: properties of ordered monoids.

    {lex,colex,symlex,revlex}_zero_is_{min,max,bound},
    {lex,colex,symlex,revlex}_br_monoid_compat_{l,r},
    {lex,colex,symlex,revlex}_monomial_order.
Add defs graded, gr{lex,colex,symlex,revlex}.
Add graded_l.

Signed-off-by: François Clément <francois.clement@inria.fr>

Add {lex,colex,symlex,revlex}_{nil,S},
    {lex,colex,symlex,revlex}_{irrefl,trans,conn},
    {lex,colex,symlex,revlex}_{strict_partial_order,strict_total_order}.

Rename modus_ponens2 -> modus_ponens_and.
Add modus_ponens_or.

Monoid_compl:
Add defs connected_alt{,_contra},
         plus_is_reg_{l,r}, zero_is_{max,bound}.
Modif defs bin_rel_monoid_compat_{l,r}, monomial_order.
Rename monomial_order_plus_compat_{l,r} -> monomial_order_br_plus_compat_{l,r}.
Rm useless monomial_order_zero_is_min.
Add conn_equiv_contra, plus_is_reg_equiv,
    bin_rel_plus_compat_reg_{l,r}, bin_rel_plus_compat_is_reg_{l,r},
    monomial_order_conn_alt{,_contra}, monomial_order_zero_is_bound,
    monomial_order_br_plus_reg_{l,r}, monomial_order_plus_is_reg_{l,r},
    bin_rel_plus_{compat,reg}_{l,r}_conv, zero_is_{min,max,bound}_conv,
    bin_rel_monoid_compat_{l,r}_conv, monomial_order_conv.

Add modus_ponens2, eq_sym_equiv.

Monoid_compl:
Rm useless strict_preorder (= strict_partial_order),
   monomial_order (for large ineq).
Rename irrefl_asym -> irrefl_asym_w_trans,
       strict_monomial_order* -> monomial_order*.
Add asym_antisym, irrefl_asym_w_antisym, asym_equiv,
    conn_equiv, str_conn_conn,
    {refl,irrefl,sym,antisym,asym,trans,conn,str_conn}_conv,
    {partial_equivalence_relation,equivalence_relation}_conv,
    {preorder,total_preorder,partial_order,total_order}_conv,
    {strict_partial_order,strict_total_order}_conv,
    bin_rel_monoid_compat_equiv,
    monomial_order_br_monoid_compat_{r,l}, monomial_order_zero_is_min.

multi_index:
Maj suggestions.

This should be in a separate file?

bof...

Signed-off-by: Houda Mouhcine <houda.mouhcine@inria.fr>

# Conflicts:
#	FEM/FE_LagP.v

Rename gmS_{injS,bijS}_sub_equiv_alt -> gmS_{injS,bijS}_val_equiv,
       lmS_{injS,bijS}_sub_equiv_alt -> lmS_{injS,bijS}_val_equiv,
       lmS_{injS,bijS}_sub_equiv -> lmS_{injS,bijS}_val_equiv_alt,
       lmS_bijS_sub_full_equiv -> lmS_bijS_val_full_equiv,
       lmS_bijS_sub_gather_equiv -> lmS_bijS_val_gather_equiv.