proposition: Theorem example_for_subst : forall (a b c d:nat), a = b+c -> c = 1 -> a+b = d -> 2*a = d+c.
proof: Proof. intros a b c d H H1 H2. subst a. subst. lazy delta [mult] iota zeta beta; rewrite Nat.add_0_r; repeat rewrite <- Nat.add_assoc; trivial. Qed.
imports: ZArith List Arith Lia