Proof of PNNetwork.boxProd preserving SimplePN

[chi-p-3141]

The proof is pretty long and probably doesn't need to be, but it works. Any suggestions to make it nicer would be welcome. (ie ways to do simultaneous simp on only two specific hypotheses)

Going to try to do the same lemma in PNNetworkExperimental if I can wrap my head around heterogeneous equalities.

[Shreyas4991]

Formatting notes on case splits and indentation of the proofs of individual cases and have statements.

[Shreyas4991]

When starting a case analysis using cases or constructors, you should use the case selector notation. For constructor, by_cases, split, and split_ifs, the . case selector is preferred although you can also use case <case name from goal state> <additional variable introduced in this case> => proof. For cases .. with and induction .. with I suggest using the code action that vscode shows (keyboard shortcut : Ctrl + . and letting it create the arms of the proof for you. In either case the proof of the case is indented more than the proof outside. Similarly proofs of haves should have an extra indentation to clearly show that they are proofs of the have statements.