proposition: Lemma normalize_aux n: (forall b a x y, 2*size x + size y < n -> equal (plus (VLSet_to_X b) (dot (dot (VLst_to_X a) x) y)) (VLSet_to_X (norm_aux n b a x y)))%nat /\ (forall b a y, size y < n -> equal (plus (VLSet_to_X b) (dot (VLst_to_X a) y)) (VLSet_to_X (norm_aux' n b a y)))%nat.
proof: Proof. induction n; split; intros; try elim (Nat.nlt_0_r _ H); destruct IHn as [IHnorm_aux IHnorm_aux']. destruct x; simpl in *. rewrite dot_neutral_right; apply IHnorm_aux'; lia. rewrite dot_ann_right, dot_ann_left, plus_com; apply plus_neutral_left. rewrite <- IHnorm_aux, ! dot_assoc; trivial; simpl; lia. rewrite <- 2 IHnorm_aux, dot_distr_right, dot_distr_left; trivial; lia. rewrite <- IHnorm_aux'. rewrite VLst_add. reflexivity. lia. destruct y; simpl in *. rewrite dot_neutral_right. symmetry. apply VLSet_add. rewrite dot_ann_right, plus_com; apply plus_neutral_left. rewrite <- IHnorm_aux, dot_assoc; trivial; lia. rewrite <- 2 IHnorm_aux', dot_distr_right; trivial; lia. rewrite VLSet_add. rewrite VLst_add. reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)