nat_ord:
Add and prove ltn_asym. ord_compl: Add and prove ord_leq_{refl,antisym,trans}, ord_ltn_{irrefl,asym,trans,total_strict}. Finite_family: Propagate new API (from ord_compl).
Loading
Please register or sign in to comment
Add and prove ltn_asym. ord_compl: Add and prove ord_leq_{refl,antisym,trans}, ord_ltn_{irrefl,asym,trans,total_strict}. Finite_family: Propagate new API (from ord_compl).