proposition: Lemma left_child_inj: forall i j, left_child i = left_child j -> i = j.
proof: Proof. unfold left_child; intros; lia. Qed.
imports: Psatz List Arith.Div2 Even Relations RelationClasses PeanoNat Peano_dec Recdef Sorting Permutation Multiset