proposition: Lemma tree_rec_bool h1 (f := tree_rec h1 id (fun a b => (cmin a b))): (forall x, natp x -> h1 x <=c \1c) -> (forall x, treep x -> f x <=c \1c).
proof: Proof. have Hb v: inc v \2c <-> v <=c \1c. apply: (iff_trans (iff_sym (NltP NS2 v))). rewrite - succ_one; exact:(cltSleP NS1). move => Ha x xT; apply/Hb; apply:tree_recdef_stable => //. by move => n nn; apply/Hb; apply: Ha. by move => u v u1 u2; rewrite /cmin/Gmin; Ytac w. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)