Add strict_weak_order_equiv_trans_incompar.
Simplify proof of strict_weak_order_equiv_incompar.

Proofs of extF_ind_{l,r} (= aliases for extF_lift_S and extF_widenF_S).
Hide admits, that are actually not used.

# Conflicts:
#	FEM/Compl/Binary_relation.v

Mv br_not from logic_compl to Binary_relation.
Mv FF stuff from Binary_relation to Finite_family.

WIP: lex_S_alt.

WIP: lex_S_alt.

node_ref_aux -> node_ref.
node_ref -> node_ref_alt.

Only define graded forms for *lexF.

    *lexT_{partial,total}_order.
Modify *lexF_strict_{partial,total}_order (were *lex_strict_{partial,total}_order).

Modify {symlex,revlex}_trans.

Add neq_sym_equiv.

Binary_relation:
Modify {lex,colex}, *lex_nil, *lexF_irrefl (were *lex_irrefl),
       {lex,colex}F_conn_alt (were *lex_conn_alt).
Rename *lex_conn -> *lexF_conn.
Add *lex{F,T}, *lexT_{refl,antisym}.
WIP: {lex,colex}_trans, *lex_*order.

Monoid_compl:
WIP: section Lex_monomial_order_Facts1.
Modify gr*lex.

WIP: true?

WIP: trans_incomp_rev, total_preorder_compl.
Add equiv_rel_incomp, strict_weak_order_equiv_incomp.

Add fun_ext2, fun_ext2_rev, imp3_imp_equiv.

Binary_relation:
Mv stuff around.
Rm {refl,irrefl,antisym,asym,conn,str_conn}_compl.
Add conv_inj, compl_inj,
    {conv,compl}_{comp,incomp}, {comp,incomp}_{conv,compl},
    comp_idem, incomp2, comp_incomp, incomp_comp,
    {refl,irrefl}_compl_equiv, trans_incomp,
    {comp,incomp}_{refl,irrefl}_equiv, {comp,incomp}_sym,
    strict_weak_order_conv{,_equiv},
    total_preorder_conv_compl, strict_weak_order{,_conv}_compl.
WIP: total_preorder_compl.

       zero_is_{min,max} -> zero_is_{left,right},
       bin_rel_monoid_compat_{min,max} -> bin_rel_monoid_compat_{zl,zr},
       monomial_order_{incr,decr} -> monomial_order_{zl,zr}.

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.