proposition: Lemma weak_heapOrdered2_postpend: forall (L : list A) x, heapOrdered L <-> weak_heapOrdered2 (L ++ (x :: nil)) (length L).
proof: Proof. intros L x. rewrite hOhO2. split. * split; repeat intro. + assert (i < length (L ++ (x :: nil))) by (apply nth_error_Some; congruence). rewrite app_length in H3. simpl in H3. assert (i < length L) by lia. generalize (parent_le i); intro. rewrite nth_error_app1 in H1; try lia. rewrite nth_error_app1 in H2; try lia. eapply H; eauto. + assert (gs < length (L ++ x :: nil)) by (apply nth_error_Some; congruence). rewrite app_length in H5. simpl in H5. destruct gs. destruct L. simpl in *. inversion H3. inversion H4. subst. reflexivity. discriminate. assert (parent (S gs) < S gs). apply parent_dec. unfold root_idx. lia. lia. * repeat intro. assert (i < length L) by (apply nth_error_Some; congruence). destruct H. apply H with i; auto. lia. rewrite nth_error_app1; trivial. rewrite nth_error_app1; trivial. apply nth_error_Some; congruence. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset