Project 'mayero/coq-num-analysis' was moved to 'mayero/rocq-num-analysis'. Please update any links and bookmarks that may still have the old path.

Commit a3e3422f authored 7 months ago by François Clément

Add nat_sub_r_monot,

    rev_ord_monot.
Proof of rev_insert_ord.

parent e242e931

Branches