proposition: Lemma le_tree_rewrite : forall (x:nat), le_tree x = SUP (fun y => if le_lt_dec x y then ZT nat else le_tree y).
proof: Proof. intro x. rewrite <- (@le_tree_rewrite_aux (S x) x). simpl. apply sup_eq. apply functional_extensionality. intro y. destruct (le_lt_dec x y). auto. apply le_tree_rewrite_aux. firstorder. firstorder. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)