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