proposition: Lemma size_5: forall u v w y z x : exp, exp_size x <= exp_size (If v y z) -> forall x0 : exp, exp_size x0 <= exp_size (If w y z) -> exp_size (If u x x0) < exp_size (If (If u v w) y z).
proof: Proof. intros u v w y z x l x0 l0. simp exp_size. rewrite <- Nat.mul_assoc. apply mult_lt_compat_l; auto. eapply Nat.le_lt_trans with (1 + exp_size (If v y z) + exp_size (If w y z)). lia. simp exp_size. simpl. rewrite Nat.mul_add_distr_r. generalize (exp_size_pos y). lia. Qed.
imports: Equations(Equations) List Program.Syntax Arith Lia