proposition: Lemma size_6: 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) -> forall x1 : exp, exp_size x1 <= exp_size (If u x x0) -> exp_size x1 <= exp_size (If (If u v w) y z).
proof: Proof. intros u v w y z x l x0 l0 x1 l1. simp exp_size. transitivity (exp_size (If u x x0)); auto. simp exp_size. simp exp_size in *. rewrite <- Nat.mul_assoc. apply mult_le_compat_l. transitivity (1 + (exp_size v * (1 + exp_size y + exp_size z)) + (exp_size w * (1 + exp_size y + exp_size z))). lia. lia. Defined.
imports: Equations(Equations) List Program.Syntax Arith Lia