proposition: Lemma aux_le_tree_aux : forall n m y, n > y -> m > y -> ltree_aux n y = ltree_aux m y.
proof: Proof. intro n. induction n. intros. inversion H. intro m. induction m. intros. inversion H0. intros. simpl. apply sup_eq. apply functional_extensionality. intro z. destruct (le_lt_dec y z). auto. apply IHn. lia. lia. Qed.
imports: Coq(Arith Relations Lia) Coq(FunctionalExtensionality)