Add antisym_equiv, asym_equiv, conn_equiv, conn_alt_equiv, str_conn_equiv.

Add br_and, br_or, br_and_conv,
    compar_equiv, incompar_equiv,
    {refl,sym,trans}_br_and_conv,
    equiv_rel_br_and_conv, preorder_equiv_rel.

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.