Add resource proof to examples/shor/Main.v

[khieta]

The two main proofs in examples/shor/Main.v are currently end_to_end_shors_correct which says that end_to_end_shors returns a factor (or nothing) and end_to_end_shors_fails_with_low_probability which says that it returns a factor with probability poly-log in the input N. We should also add a lemma end_to_end_shors_resource_bound about the number of gates it requires, per the proofs in examples/shor/ResourceShor.v.