i need a dafny coder -- 2

/* Question/Exercise 2 of 4 */
lemma Q2_DistributivityOfSetUnionOverSetIntersection(A: set, B: set, C: set)
ensures A+(B*C) == (A+B)*(A+C)
/*
In this exercise you are expected to write a *full* proof for the lemma;
as an example, see the proof of "DistributivityOfSetIntersectionOverSetUnion"
starting on line 167 of lecture04.dfy and continuing on lines 3-44 of tutorial04.dfy;
note that the proof must be fully justified for the human reader,
with labels to assertions and the relevant reveal statements where needed,
as can be seen in the "Distributivity2a" lemma from the tutorial
(in contrast to the lemma "Distributivity1a" from the lecture, where we did not add labels);
in case of syntax errors, you solution will NOT be checked.

YOUR_SOLUTION_SHOULD_BE_WRITTEN_BELOW_THIS_LINE, between curly braces "{" and "}" */


/* Question/Exercise 3 of 4 */
lemma Q3_SetUnionIsAssociative(A: iset, B: iset, C: iset)
ensures (A + B) + C == A + (B + C)
/*
when taking the union of three (possibly-infinite) sets, the order of the operations does not matter;
this property is known as associativity;
this is the same in the addition of integers:

assert forall x:int, y: int, z: int :: x+(y+z) == (x+y)+z;

(whereas for sutraction it does not hold: assert 10-(4-1) == 10-3 == 7 != 5 == 6-1 == (10-4)-1;)

As in exercise 2 above, you are expected to provide a *full* proof, in Dafny, with no errors.

YOUR_SOLUTION_SHOULD_BE_WRITTEN_BELOW_THIS_LINE, between curly braces "{" and "}" */


/* Question/Exercise 4 of 4 */
lemma preparation_for_Q4_SetDifferenceIs_NOT_Associative()
ensures !forall A: set<int>, B: set<int>, C: set<int> :: (A - B) - C == A - (B - C)
{
assert exists A: set<int>, B: set<int>, C: set<int> :: (A - B) - C != A - (B - C) by {
var A, B, C := Q4_Evidence_That_SetDifferenceIs_NOT_Associative();
assert (A - B) - C != A - (B - C);
}
}

lemma Q4_Evidence_That_SetDifferenceIs_NOT_Associative() returns (A: set<int>, B: set<int>, C: set<int>)
ensures (A - B) - C != A - (B - C)
/*
Recall from "SquareOfIntegersIsNotMonotonic" in lecture05.dfy how a lemma that returns results
can be used to disprove a claim by providing evidence for its negation;
similarly, your goal here is to choose values for A,B,C and demonstrate (using assertions or the "calc" construct)
how when performing the set difference operation twice, the order of operations DOES matter!

YOUR_SOLUTION_SHOULD_BE_WRITTEN_BELOW_THIS_LINE, between curly braces "{" and "}" */