proposition: Lemma tree_size_p: [/\ (forall x, natp x -> tree_size (Tb x) = x), (forall x, treep x -> tree_size (Tp x) = tree_size x) & (forall x y, treep x ->treep y -> tree_size (Tx x y) = cmax (tree_size x) (tree_size y)) ].
proof: Proof. rewrite /tree_size;split. - by move => n nN; rewrite tree_recdef_pb'. - by move => x xt; rewrite tree_recdef_pp. - by move => x y xt yt; rewrite tree_recdef_px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)