proposition: Lemma parent_right_child: forall i, parent (right_child i) = i.
proof: Proof. unfold parent, right_child, left_child. intro. replace (1 + i + i + 1 - 1) with (S (2 * i)) by lia. apply div2_double_plus_one. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset