proposition: Lemma af_le : SecureBy (fun x y => x <= y) (SUP le_tree).
proof: Proof. rewrite sup_rewrite. apply (@well_founded_induction nat lt). apply lt_wf. intros. unfold le_tree. simpl. intro y. destruct (le_lt_dec x y). simpl. intros. right. right. apply l. rewrite -> le_tree_rewrite_aux. eapply sec_strengthen. 2: { apply H. apply l. } intros. simpl. simpl in H0. destruct H0. left. left. apply H0. right. left. apply H0. firstorder. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)