proposition: Lemma wzero_combine {sz sz'} : forall (w0: word sz) (w1: word sz'), combine w0 w1 = wzero _ -> w0 = wzero _ /\ w1 = wzero _.
proof: Proof. intros * H. pose proof (f_equal (@split1 sz sz') H). pose proof (f_equal (@split2 sz sz') H). rewrite split1_combine, split1_wzero in H0. rewrite split2_combine, split2_wzero in H1. intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation