Function lemma_whole_fraction_has_no_frame

pub proof fn lemma_whole_fraction_has_no_frame(a: FractionRA)

Expand description

requires

a == FractionRA::Frac(1 as real),

ensures

forall |b: FractionRA| !FractionRA::op(a, b).valid(),

lemma_whole_fraction_has_no_frame