proposition: Lemma root_minimal: forall L, heapOrdered L -> forall r, nth_error L root_idx = Some r -> Forall (fun x => r <<= x) L.
proof: Proof. unfold root_idx. do 4 intro. rewrite Forall_forall. intros. apply In_nth_error in H1. destruct H1 as [i H1]. remember i as j. assert (j <= i) by (subst j; constructor). clear Heqj. revert j x H2 H1. induction i. destruct j. intros. rewrite H0 in H1. inversion H1. reflexivity. inversion 1. intros. assert (j <= i \/ j = S i) by lia. destruct H3. eapply IHi; eauto. subst j. destruct (nth_error_le _ _ _ H1 (parent (S i))). generalize (parent_dec (S i)). unfold root_idx. lia. transitivity x0. eapply IHi. 2: apply H3. generalize (parent_dec (S i)). unfold root_idx. lia. rewrite hOhO2 in H. eapply H; eauto. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset