I want to prove that when receiving a binary search tree as an argument, the [insert] function generates another binary search tree. Insert Function: Fixpoint insert {V : Type} (x : key) (v : V) (t : ...

I want to create a Coq tactic that looks something like the following. I assert a proposition named H, I prove that proposition, and then I use simpl within that proposition. The tactic would look som...

I'm trying to use ntheorem to complete proofs, but having some problems because it has been not possible to replace the \qedsymbol after an enumerate group and at the end of an align* group, the \qed ...

fun perfect(n) = let fun add_factors(n) = let fun f(i) = if n mod i = 0 then i else 0; fun sum(a, b) = if a > b then 0 ...