fact: Fixpoint ins x s := match s with | Leaf => Node Red Leaf x Leaf | Node c a y b => if x < y then balance c (ins x a) y b else if y < x then balance c a y (ins x b) else Node c a x b end.
imports: mathcomp(ssreflect ssrnat ssrbool eqtype)